theorem Hex.GraphIso.Nauty.Sparse.pairs_advance {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (tcLevel fuel cfuel level numcells tc tv1 tv index : Nat) (first : Bool) (cell : VSet n) (st : State n) (exit : Generic.Exit) (hl : 1 ≤ level) (hpairs : PairsOk G st) (h : PairsReady G tcLevel level numcells (Generic.Policy.recover (n + 2) level st)) (ht : Generic.Target State.frame level tc cell (Generic.Policy.recover (n + 2) level st)) (hrecord : CheapRecorded level tc (Generic.Policy.recover (n + 2) level st)) (hpast : ∀ (smaller : VSet n), Generic.Past first tv1 (smaller.nextElem (some tv))) : PairsOk G (Generic.advance (n + 2) (fun (first : Bool) (level numcells tc tv1 : Nat) (cursor : Option Nat) (cell : VSet n) (index : Nat) (st : State n) => Generic.sweep first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index st) first level numcells tc tv1 tv cell index st exit).snd.snd

A valid returned workspace and the recovered native sweep invariants suffice for every resume and nonlocal exit through the actual filters.

theorem Hex.GraphIso.Nauty.Sparse.firstPath_pairs {n k : Nat} {G : Sparse.Colored n k} (hn : 0 < n) {tcLevel fuel level numcells last : Nat} {st leaf : State n} (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel level numcells st last leaf) (hl : 1 ≤ level) (hi : NodeInv G level numcells st) (hshape : FirstShape G.graph level numcells st) (htsize : n < st.firsttc.size) (hcsize : n + 1 < st.firstcode.size) (hblank : st.canong.toRows = (Graph.ofGraph G.graph).blank) (hwork : st.workperm.size = n) (htrace : TraceOk G st) (hpairs : PairsOk G st) (hpath : PathInv G level st) (hboundary : CheapBoundary G level st) (hbound : st.noncheaplevel ≤ level) : PairsOk G (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd

The complete first-path search preserves the pruning workspace. All explicit admissions use proved native automorphisms; implicit admissions use boundaries established at actual equitable states and retained across calls.