structure Hex.GraphIso.Nauty.Sparse.Saved {n k : Nat} (G : Sparse.Colored n k) (st : State n) : Prop

The installed references and workspace needed to interpret an actual automorphism verdict. This asserts validity, independently of maximality or generator soundness.

• first : st.firstlab.size = n ∧ CellsReach G.toDense st.firstlab
• canonical : CanonLabel G st
• store : Store G.graph st
• work : st.workperm.size = n

theorem Hex.GraphIso.Nauty.Sparse.Saved.congr {n k : Nat} {G : Sparse.Colored n k} {st out : State n} (h : Saved G st) (hf : out.firstlab = st.firstlab) (hc : out.canonlab = st.canonlab) (hs : Store G.graph out) (hw : out.workperm.size = st.workperm.size) : Saved G out

theorem Hex.GraphIso.Nauty.Sparse.Saved.visit {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : Saved G st) (level numcells : Nat) : Saved G (Sparse.visit (Graph.ofGraph G.graph) level numcells st).snd.snd

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

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

theorem Hex.GraphIso.Nauty.Sparse.Saved.classify {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : Saved G st) (level numcells : Nat) (l : Label n) (hl : Label.ofArray? n st.lab = some l) : Saved G (Sparse.classify (Graph.ofGraph G.graph) level numcells st).snd

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

theorem Hex.GraphIso.Nauty.Sparse.Saved.child {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : Saved G st) (first : Bool) (level tc tv : Nat) : Saved G (Generic.Policy.child first level tc tv st)

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

theorem Hex.GraphIso.Nauty.Sparse.Saved.leave {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : Saved G st) (tv : Nat) : Saved G (Generic.Policy.leaveChild tv st)

theorem Hex.GraphIso.Nauty.Sparse.Saved.recover {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : Saved G st) (inf level : Nat) : Saved G (Generic.Policy.recover inf level st)

theorem Hex.GraphIso.Nauty.Sparse.Saved.leaf {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : Saved G st) {level numcells : Nat} (hr : Ready G level numcells st) (leaf : Leaf) (hc : ∀ (sr : Nat), leaf = Generic.Leaf.better sr → Candidate G.graph st sr) : Saved G (leafExit leaf level st).snd

A leaf can replace its incumbent with the reached current label while retaining all reference, native row-prefix and workspace guarantees.

theorem Hex.GraphIso.Nauty.Sparse.Saved.node {n k : Nat} {G : Sparse.Colored n k} {st : State n} (h : Saved G st) (hn : 0 < n) (tcLevel fuel level numcells : Nat) (hl : 1 ≤ level) (hi : NodeInv G level numcells st) : Saved G (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd

All the saved validity facts survive a complete off-path call using the independent reference, frame, cache and allocation theorems.

theorem Hex.GraphIso.Nauty.Sparse.firstPath_ready {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells last : Nat} {st leaf : State n} (hn : 0 < n) (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel level numcells st last leaf) (hl : 1 ≤ level) (hi : NodeInv G level numcells st) : Ready G last n leaf

The actual first path reaches a native discrete prepared leaf, with its original colour-cell reachability and cache invariant intact.

theorem Hex.GraphIso.Nauty.Sparse.firstPath_saved {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells last : Nat} {st leaf : State n} (hn : 0 < n) (hl : 1 ≤ level) (hi : NodeInv G level numcells st) (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel level numcells st last leaf) (hb : st.canong.toRows = (Graph.ofGraph G.graph).blank) (hw : st.workperm.size = n) : Saved G (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd

The completed actual first path supplies both valid reference labels and the installed native row prefix for subsequent admissions.