def Hex.GraphIso.Nauty.Sparse.CheapHistory {n : Nat} (G : SparseGraph n) (tcLevel level agreed numcells : Nat) (st : State n) : Prop

Whenever the cheap guard admits the frozen first ancestor, its actual saved descent and the current aligned native descent remain available.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.CheapHistory.transport {n : Nat} {G : SparseGraph n} {tcLevel level agreed numcells : Nat} {st out : State n} {level' agreed' numcells' : Nat} (h : CheapHistory G tcLevel level agreed numcells st) (hr : SearchState.reference out = SearchState.reference st) (hg : out.gcaFirst = st.gcaFirst) (hn : out.noncheaplevel ≤ st.gcaFirst → st.noncheaplevel ≤ st.gcaFirst) (hd : ∀ (last : Nat), Depth last st → Depth last out) (ha : ∀ (root : RefineSt n), Aligned G st.gcaFirst root level agreed numcells st → Aligned G st.gcaFirst root level' agreed' numcells' out) : CheapHistory G tcLevel level' agreed' numcells' out

theorem Hex.GraphIso.Nauty.Sparse.CheapHistory.compare {n : Nat} {G : SparseGraph n} {tcLevel level numcells : Nat} {st : State n} (h : CheapHistory G tcLevel level (level - 1) numcells st) (hl : 0 < level) {code : Nat} (hc : code < codeSentinel) : CheapHistory G tcLevel level level numcells (compareCodes level code st)

theorem Hex.GraphIso.Nauty.Sparse.CheapHistory.target {n : Nat} {G : SparseGraph n} {tcLevel level numcells : Nat} {st : State n} (h : CheapHistory G tcLevel level level numcells st) : CheapHistory G tcLevel level level numcells (chooseTarget false (Graph.ofGraph G) tcLevel level numcells st).snd.snd.snd

theorem Hex.GraphIso.Nauty.Sparse.CheapHistory.classify {n : Nat} {G : SparseGraph n} {tcLevel level numcells : Nat} {st : State n} (h : CheapHistory G tcLevel level level numcells st) : CheapHistory G tcLevel level level numcells (Sparse.classify (Graph.ofGraph G) level numcells st).snd

theorem Hex.GraphIso.Nauty.Sparse.CheapHistory.leaf {n : Nat} {G : SparseGraph n} {tcLevel level numcells : Nat} {st : State n} (h : CheapHistory G tcLevel level level numcells st) (leaf : Leaf) : CheapHistory G tcLevel level level numcells (leafExit leaf level st).snd

theorem Hex.GraphIso.Nauty.Sparse.CheapHistory.cheap {n : Nat} {G : SparseGraph n} {tcLevel level numcells : Nat} {st : State n} (h : CheapHistory G tcLevel level level numcells st) (first : Bool) (hg : st.gcaFirst ≤ level) : CheapHistory G tcLevel level level numcells (cheapCheck first level st)

def Hex.GraphIso.Nauty.Sparse.CheapRecorded {n : Nat} (level tc : Nat) (st : State n) : Prop

A sweep target agrees with the first target when its ancestor is cheap and the live code comparison still reaches this level.

Equations

• Hex.GraphIso.Nauty.Sparse.CheapRecorded level tc st = (st.noncheaplevel ≤ st.gcaFirst → st.eqlevFirst = level → st.firsttc[level]! = Int.ofNat tc)

theorem Hex.GraphIso.Nauty.Sparse.CheapRecorded.cheap {n level tc : Nat} {st : State n} (h : CheapRecorded level tc st) (first : Bool) (hg : st.gcaFirst ≤ level) : CheapRecorded level tc (cheapCheck first level st)

theorem Hex.GraphIso.Nauty.Sparse.CheapHistory.recorded {n : Nat} {G : SparseGraph n} {tcLevel level numcells : Nat} {st : State n} (h : CheapHistory G tcLevel level level numcells st) (hnc : numcells < n) (hs : Scratch.Valid n st.lab st.ptn level st.canong.scratch) : have r := chooseTarget false (Graph.ofGraph G) tcLevel level numcells st; CheapRecorded level r.fst.toNat r.snd.snd.snd

The native cached selector records the target needed for every next child whenever its frozen cheap history stays active.

theorem Hex.GraphIso.Nauty.Sparse.CheapHistory.child {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells tc tv : Nat} {st : State n} {cell : VSet n} (h : CheapHistory G.graph tcLevel level level numcells st) (first : Bool) (hok : Ready G level numcells st) (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (hrecord : CheapRecorded level tc st) : have next := Generic.Policy.child first level tc tv st; have r := visit (Graph.ofGraph G.graph) (level + 1) (numcells + 1) next; CheapHistory G.graph tcLevel (level + 1) level r.fst r.snd.snd

A stored sweep target extends the current history through the actual native individualization and its cached child refinement.

theorem Hex.GraphIso.Nauty.Sparse.CheapHistory.child_return {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells tc tv : Nat} {st : State n} {cell : VSet n} (h : CheapHistory G.graph tcLevel level level numcells st) (first : Bool) (hg : st.gcaFirst ≤ level) (hl : 1 ≤ level) (hok : Ready G level numcells st) (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) : have out := (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Generic.Policy.child first level tc tv st)).snd; have result := Generic.Policy.recover (n + 2) level (Generic.Policy.leaveChild tv out); CheapHistory G.graph tcLevel level level numcells result ∧ (CheapRecorded level tc st → CheapRecorded level tc result)

An actual off-path child preserves both the frozen cheap history and the parent's recorded target after leaving the child and recovering the native partition and cache. This holds even for a truncated child call.

theorem Hex.GraphIso.Nauty.Sparse.CheapHistory.first_iso {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st out : State n} {l f : Label n} (h : CheapHistory G.graph tcLevel level level numcells st) (hauto : Sparse.classify (Graph.ofGraph G.graph) level numcells st = (Generic.Leaf.autoFirst, out)) (hw : st.workperm.size = n) (hl : Label.ofArray? n st.lab = some l) (hf : Label.ofArray? n st.firstlab = some f) (hrl : CellsReach G.toDense st.lab) (hrf : CellsReach G.toDense st.firstlab) : Sparse.IsIso G G (l.perm.comp f.perm.inv) ∧ ∀ (v : Fin n), out.workperm[↑v]! = ↑((l.perm.comp f.perm.inv).get v)

The retained native history justifies first-reference admission in both guard arms. The saved sentinel supplies the depth bound independently of the incumbent comparison invariant.