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

A native off-path entry carries both admission history and the general guided history for its next cached refinement.

• 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
• route : let r := visit (Graph.ofGraph G.graph) level numcells st; RouteHistory G.graph tcLevel level (level - 1) r.fst r.snd.snd

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

Prepared and recovered native partitions retain the histories needed to interpret both code comparisons and first-reference admission.

• 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
• route : RouteHistory G.graph tcLevel level level numcells st

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

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

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

Entering an actual child supplies the pending general and cheap histories with the child's own invalidated cache and individualized arrays.

theorem Hex.GraphIso.Nauty.Sparse.CodeReady.child_return {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells tc tv : Nat} {st : State n} {cell : VSet n} (h : CodeReady G tcLevel level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (first : Bool) (fuel : Nat) (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (hc : CheapRecorded level tc st) (hr : RouteRecorded G.graph tcLevel level tc st) : have ch := Generic.Policy.child first level tc tv st; have out := (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1) ch).snd; have back := Generic.Policy.recover (n + 2) level (Generic.Policy.leaveChild tv out); CodeReady G tcLevel level numcells back ∧ CheapRecorded level tc back ∧ RouteRecorded G.graph tcLevel level tc back

Full native child calls preserve the parent's histories and both target records after recovery. This uses independent frame and trace theorems and therefore does not assume the child's code correctness.