HexGraphIso.Nauty.Sparse.TraceFrameOps

theorem Hex.GraphIso.Nauty.Sparse.chooseTarget_trace {n : Nat} (first : Bool) (g : Graph n) (tcLevel level numcells : Nat) (st : State n) :

(chooseTarget first g tcLevel level numcells st).snd.snd.snd.genTrace = st.genTrace

Cached target selection does not append to or replace the trace.

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.visit {n k : Nat} {G : Sparse.Colored n k} {base cells level numcells : Nat} {root st : State n} (h : TraceFrame G base root st) (hp : Ready G base cells root) (hi : NodeInv G level numcells st) (hn : 0 < n) (hb : 1 ≤ base) (hlevel : base < level) :

A native visit below the frozen ancestor preserves its references and trace while refining the current partition inside the ancestor cells.

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.record {n k : Nat} {G : Sparse.Colored n k} {base : Nat} {root st : State n} (h : TraceFrame G base root st) (level code : Nat) :

TraceFrame G base root (recordFirst level code st)

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.compare {n k : Nat} {G : Sparse.Colored n k} {base : Nat} {root st : State n} (h : TraceFrame G base root st) (level code : Nat) :

TraceFrame G base root (compareCodes level code st)

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.target {n k : Nat} {G : Sparse.Colored n k} {base : Nat} {root st : State n} (h : TraceFrame G base root st) (first : Bool) (tcLevel level numcells : Nat) :

TraceFrame G base root (chooseTarget first (Graph.ofGraph G.graph) tcLevel level numcells st).snd.snd.snd

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.cheap {n k : Nat} {G : Sparse.Colored n k} {base : Nat} {root st : State n} (h : TraceFrame G base root st) (first : Bool) (level : Nat) :

TraceFrame G base root (cheapCheck first level st)

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.terminal {n k : Nat} {G : Sparse.Colored n k} {base cells level numcells : Nat} {root st : State n} (h : TraceFrame G base root st) (hp : Ready G base cells root) (hr : Ready G level numcells st) (hn : 0 < n) (hb : 1 ≤ base) (hlevel : base ≤ level) :

TraceFrame G base root (firstterminal level st)

Installing a first leaf places both references in the current labels, which the incoming frame already locates inside the suspended ancestor.

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.child {n k : Nat} {G : Sparse.Colored n k} {base cells level numcells : Nat} {root st : State n} (h : TraceFrame G base root st) (hp : Ready G base cells root) (hr : Ready G level numcells st) (hn : 0 < n) (hb : 1 ≤ base) (hlevel : base ≤ level) (first : Bool) {tc tv : Nat} {cell : VSet n} (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) :

TraceFrame G base root (Generic.Policy.child first level tc tv st)

Actual individualization stays inside every suspended ancestor frame, retaining its references and all previously emitted stabilizers.

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.afterChild {n k : Nat} {G : Sparse.Colored n k} {base : Nat} {root st : State n} (h : TraceFrame G base root st) (level tv : Nat) :

TraceFrame G base root (afterChildFirst level tv st)

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.leave {n k : Nat} {G : Sparse.Colored n k} {base : Nat} {root st : State n} (h : TraceFrame G base root st) (tv : Nat) :

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.recover {n k : Nat} {G : Sparse.Colored n k} {base cells level : Nat} {root st : State n} (h : TraceFrame G base root st) (hp : Ready G base cells root) (hn : 0 < n) (hb : 1 ≤ base) (hlevel : base ≤ level) (hbound : level ≤ n) :

Recovering a still-active ancestor preserves every coarser frozen frame and its references; the invalidated sparse cache retains its bounds.

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.afterSweep {n k : Nat} {G : Sparse.Colored n k} {base : Nat} {root st : State n} (h : TraceFrame G base root st) (first : Bool) (level size index : Nat) :

TraceFrame G base root (Generic.Policy.afterSweep first level size index st)