theorem Hex.GraphIso.Nauty.Sparse.fixedPolicy {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (tcLevel : Nat) : Generic.CallPolicy (Graph.ofGraph G.graph) (n + 2) tcLevel (fixedContract G)

Actual sparse node and sweep calls restore their fixed-point bitsets. The recursion uses the independently proved native frame effects.

theorem Hex.GraphIso.Nauty.Sparse.node_fixed {n k : Nat} {G : Sparse.Colored n k} (hn : 0 < n) (first : Bool) (tcLevel fuel level numcells : Nat) (st : State n) (hl : 1 ≤ level) (h : NodeInv G level numcells st) (hf : FixedCells level st.frame) : (Generic.node first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd.fixedpts = st.fixedpts

Every production node restores its incoming fixed vertices, including operational truncation and returns that unwind past several ancestors.

theorem Hex.GraphIso.Nauty.Sparse.sweep_fixed {n k : Nat} {G : Sparse.Colored n k} (hn : 0 < n) (first : Bool) (tcLevel fuel cfuel level numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : State n) (hl : 1 ≤ level) (h : Ready G level numcells st) (ht : Generic.Target State.frame level tc cell st) (hv : ∀ (v : Nat), cursor = some v → cell.mem v = true) (hf : FixedCells level st.frame) : (Generic.sweep first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd.fixedpts = st.fixedpts

Every production sweep restores its incoming fixed vertices, including all orbit skips, short and long filters, and nonlocal exits.

theorem Hex.GraphIso.Nauty.Sparse.runColored_fixed {n k : Nat} (G : Sparse.Colored n k) : (runColored G).fixedpts = VSet.empty

The completed initialized search has removed every temporary fixed vertex. All root validity and singleton premises follow from initialization.