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

The executed sparse policy meets the shared mutual recursion's complete partition, equitable-parent, colour-reachability and scratch contract.

theorem Hex.GraphIso.Nauty.Sparse.node_frame {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) : FrameOut G (level - 1) level st (Generic.node first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd

Every production node preserves its caller's partition frame, including truncated calls and nonlocal returns.

theorem Hex.GraphIso.Nauty.Sparse.sweep_frame {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) : FrameOut G level level st (Generic.sweep first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd

theorem Hex.GraphIso.Nauty.Sparse.runState_frame {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; FrameOut G 0 1 (initial (Graph.ofGraph G.graph) p.fst p.snd) (runState (Graph.ofGraph G.graph) p.fst p.snd).snd

The actual initialized root has the production frame guarantee, with all entry hypotheses derived from its stable colour buckets.

theorem Hex.GraphIso.Nauty.Sparse.run_frame {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; FrameOut G 0 1 (initial (Graph.ofGraph G.graph) p.fst p.snd) (run (Graph.ofGraph G.graph) p.fst p.snd)

Final canonical-row installation preserves the whole production frame.