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

The production bounds are sufficient for the actual sparse mutual recursion. The frame assertions also cover calls with insufficient bounds.

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

A valid production node cannot exhaust the established level bound.

theorem Hex.GraphIso.Nauty.Sparse.sweep_noFuel {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 : n ≤ level + fuel) (hc : Generic.CursorFuel n cfuel cursor) : (Generic.sweep first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).fst ≠ Generic.Exit.fuel

theorem Hex.GraphIso.Nauty.Sparse.runState_noFuel {n k : Nat} (G : Sparse.Colored n k) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; (runState (Graph.ofGraph G.graph) p.fst p.snd).fst ≠ Generic.Exit.fuel

The pinned sparse production root never reports exhausted recursion, including order zero. Its existing n + 2 bound is sufficient unchanged.