theorem Hex.GraphIso.Nauty.Sparse.Max.FirstInput.pairs_out {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel last : Nat} {f : Frame n} {parents : Parents n} {leaf : State n} (h : FirstInput G tcLevel f parents) (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel f.level f.numcells f.entry last leaf) : PairsOk G (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel f.level f.numcells f.entry).snd

First-descent entry invariants supply valid pruning pairs throughout the complete executed first call, including its later siblings.

theorem Hex.GraphIso.Nauty.Sparse.Max.FirstInput.pairs_back {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel tv last : Nat} {f : Frame n} {parents : Parents n} {leaf : State n} {bs fs : List Nat} (h : FirstInput G tcLevel f parents) (hi : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n) (htv : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.fst.nextElem none = some tv) (path : have p := Frame.firstParent G.graph tcLevel f [] tv; Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel (Parent.child G.graph tcLevel p).level (Parent.child G.graph tcLevel p).numcells (Parent.child G.graph tcLevel p).entry last leaf) (resume : have p := Frame.firstParent G.graph tcLevel f [] tv; Resumed G tcLevel p bs fs (Parent.firstBack G.graph tcLevel fuel p) parents) : have p := Frame.firstParent G.graph tcLevel f [] tv; PairsReady G tcLevel f.level (Frame.target G.graph tcLevel f).numcells (Parent.firstBack G.graph tcLevel fuel p)

Native first-child cleanup and recovery restore the complete pruning workspace at its parent. The fixed-point set is restored literally, and the implicit-pair boundary is inherited from the actual first call.