theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.cheap_visit {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel : Nat} {l : Loop n} {bs fs : List Nat} {tv : Nat} {cell : VSet n} {st : State n} {parents : Parents n} (h : SweepInput G tcLevel l bs fs (some tv) cell st parents) (hf : l.first = true) (heq : st.eqlevFirst = l.node.level) (hcheap : st.noncheaplevel ≤ l.node.level) (hbudget : n ≤ l.node.level + fuel) : (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (l.node.level + 1) ((Loop.cell G.graph tcLevel l).numcells + 1) (Generic.Policy.child l.first l.node.level (Loop.cell G.graph tcLevel l).tc tv st)).fst = Generic.Exit.unwind l.node.level false

Every remaining child of a cheap first-path receiver reaches the saved reference and returns to this receiver. Its history is supplied by the actual sweep invariants after all preceding sibling searches.

theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.visit_level {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel target : Nat} {short : Bool} {l : Loop n} {bs fs : List Nat} {tv : Nat} {cell : VSet n} {st : State n} {parents : Parents n} (h : SweepInput G tcLevel l bs fs (some tv) cell st parents) (hf : l.first = true) (heq : st.eqlevFirst = l.node.level) (hsame : l.node.level < st.allsamelevel) (hbudget : n ≤ l.node.level + fuel) (he : (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (l.node.level + 1) ((Loop.cell G.graph tcLevel l).numcells + 1) (Generic.Policy.child l.first l.node.level (Loop.cell G.graph tcLevel l).tc tv st)).fst = Generic.Exit.unwind target short) : target = l.node.level

Every later first-path child returns to its immediate receiver. Cheap receivers use the emitted reference; other receivers use the proved bounds of the actual return, including short pruning returns.

theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.visit_return {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel : Nat} {l : Loop n} {bs fs : List Nat} {tv : Nat} {cell : VSet n} {st : State n} {parents : Parents n} (h : SweepInput G tcLevel l bs fs (some tv) cell st parents) (hf : l.first = true) (heq : st.eqlevFirst = l.node.level) (hsame : l.node.level < st.allsamelevel) (hbudget : n ≤ l.node.level + fuel) : (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (l.node.level + 1) ((Loop.cell G.graph tcLevel l).numcells + 1) (Generic.Policy.child l.first l.node.level (Loop.cell G.graph tcLevel l).tc tv st)).fst = Generic.Exit.unwind l.node.level false

A later first-path child returns normally, with no short-prune request. Sufficient fuel and the positive first ancestor exclude every other executed exit.

theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.tail_done {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel cfuel : Nat} {l : Loop n} {bs fs : List Nat} {tv1 index : Nat} {cursor : Option Nat} {cell : VSet n} {st : State n} {parents : Parents n} (h : SweepInput G tcLevel l bs fs cursor cell st parents) (hf : l.first = true) (heq : st.eqlevFirst = l.node.level) (hsame : l.node.level < st.allsamelevel) (hbudget : n ≤ l.node.level + fuel) (hcursor : Generic.CursorFuel n cfuel cursor) (hpast : Generic.Past l.first tv1 cursor) : (Generic.sweep l.first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel l.node.level (Loop.cell G.graph tcLevel l).numcells (Loop.cell G.graph tcLevel l).tc tv1 cursor cell index st).fst = Generic.Exit.done

The complete remaining first-path sweep finishes. Every surviving child returns locally, and recovery retains the first-code and all-same bounds through both native pruning filters and orbit skips.