theorem Hex.GraphIso.Nauty.Sparse.fuel_advance {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) {fuel cfuel : Nat} {next : Generic.SweepFn (State n) n} (hnext : (fuelContract G).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (st out : State n) (exit : Generic.Exit) (hl : 1 ≤ level) (h : Ready G level numcells st) (htarget : Generic.Target State.frame level tc cell st) (hx : FrameOut G level level st out) (hsafe : exit ≠ Generic.Exit.fuel) (hf : n ≤ level + fuel) (hcursor : n ≤ tv + (cfuel + 1)) : (Generic.advance (n + 2) next first level numcells tc tv1 tv cell index out exit).fst ≠ Generic.Exit.fuel

Recovery and pruning cannot introduce exhaustion after a completed child. Every subsequent packed-set cursor advances strictly.

theorem Hex.GraphIso.Nauty.Sparse.fuel_sweep {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) {fuel cfuel : Nat} {descend : Generic.NodeFn (State n)} {next : Generic.SweepFn (State n) n} (hdescend : (fuelContract G).nodeValid fuel descend) (hnext : (fuelContract G).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (st : State n) (hl : 1 ≤ level) (h : Ready G level numcells st) (htarget : Generic.Target State.frame level tc cell st) (htv : cell.mem tv = true) (hf : n ≤ level + fuel) (hcursor : n ≤ tv + (cfuel + 1)) : (Generic.sweepStep (n + 2) descend next first level numcells tc tv1 tv cell index st).fst ≠ Generic.Exit.fuel

Individualization consumes a level, and each sibling consumes a cursor position. The existing node and sweep bounds cover both recursive calls.