structure Hex.GraphIso.Nauty.Sparse.TraceEntry {n k : Nat} (G : Sparse.Colored n k) (tcLevel level numcells : Nat) (st : State n) : Prop

An off-path entry carries a pending history for its actual cached visit, together with already installed references and a sound trace.

• node : NodeInv G level numcells st
• saved : Saved G st
• trace : TraceOk G st
• ancestor : st.gcaFirst ≤ level
• history : let r := visit (Graph.ofGraph G.graph) level numcells st; CheapHistory G.graph tcLevel level (level - 1) r.fst r.snd.snd

structure Hex.GraphIso.Nauty.Sparse.TraceReady {n k : Nat} (G : Sparse.Colored n k) (tcLevel level numcells : Nat) (st : State n) : Prop

A prepared node or recovered sweep has an equitable current partition, live cheap history, valid references, and a sound emitted trace.

• ready : Ready G level numcells st
• saved : Saved G st
• trace : TraceOk G st
• ancestor : st.gcaFirst ≤ level
• history : CheapHistory G.graph tcLevel level level numcells st

theorem Hex.GraphIso.Nauty.Sparse.TraceEntry.prepare {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} (h : TraceEntry G tcLevel level numcells st) (hn : 0 < n) (hl : 1 ≤ level) : have r := prepareOther (Graph.ofGraph G.graph) tcLevel level numcells st; TraceReady G tcLevel level r.fst r.snd.snd.snd.snd.snd

theorem Hex.GraphIso.Nauty.Sparse.TraceReady.classified {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} (h : TraceReady G tcLevel level numcells st) (hn : 0 < n) : have c := classify (Graph.ofGraph G.graph) level numcells st; TraceReady G tcLevel level numcells (leafExit c.fst level c.snd).snd

Classifying and executing a leaf action preserves all validity facts, and every appended automorphism is justified by the native admission proof.

theorem Hex.GraphIso.Nauty.Sparse.TraceReady.cheap {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} (h : TraceReady G tcLevel level numcells st) (first : Bool) : TraceReady G tcLevel level numcells (cheapCheck first level st)

theorem Hex.GraphIso.Nauty.Sparse.TraceReady.child {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} (h : TraceReady G tcLevel level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (first : Bool) {tc tv : Nat} {cell : VSet n} (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (hrecord : CheapRecorded level tc st) : TraceEntry G tcLevel (level + 1) (numcells + 1) (Generic.Policy.child first level tc tv st)

theorem Hex.GraphIso.Nauty.Sparse.TraceReady.child_return {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} (h : TraceReady G tcLevel level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (first : Bool) (fuel : Nat) {tc tv : Nat} {cell : VSet n} (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (htrace : TraceOk G (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 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); TraceReady G tcLevel level numcells result ∧ (CheapRecorded level tc st → CheapRecorded level tc result)

A sound trace returned by an actual child combines with independently proved frame, cache and history effects to establish the next sweep state.