theorem Hex.GraphIso.Nauty.Sparse.breakout_node {n level numcells tc len o : Nat} {lab ptn : Array Nat} {active : VSet n} (hp : lab.toList.Perm (List.range n)) (h : NodeOk n level lab ptn active) (hc : numcells = bcount ptn level n) (hl : level ≤ numcells) (ht : IsCell ptn level tc len) (hr : tc + len ≤ n) (hn : 1 < len) (ho : o < len) : have child := breakout n lab ptn (level + 1) tc lab[tc + o]!; child.fst.toList.Perm (List.range n) ∧ NodeOk n (level + 1) child.fst child.snd.fst child.snd.snd ∧ numcells + 1 = bcount child.snd.fst (level + 1) n ∧ level + 1 ≤ numcells + 1

Every target member increases the accurate count by one and preserves the node invariants and depth bound used to exhaust the unpruned tree.

theorem Hex.GraphIso.Nauty.Sparse.specLeaves_succ {n : Nat} (G : SparseGraph n) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (hp : lab.toList.Perm (List.range n)) (h : NodeOk n level lab ptn active) (hc : numcells = bcount ptn level n) (hl : level ≤ numcells) (hf : n < fuel + numcells) : specLeaves G tcLevel (fuel + 1) level lab ptn active numcells = specLeaves G tcLevel fuel level lab ptn active numcells

Increasing an already sufficient recursion bound changes no leaf. The induction covers every target member, so no branch is silently truncated.

theorem Hex.GraphIso.Nauty.Sparse.specLeaves_add {n : Nat} (G : SparseGraph n) (tcLevel fuel extra level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (hp : lab.toList.Perm (List.range n)) (h : NodeOk n level lab ptn active) (hc : numcells = bcount ptn level n) (hl : level ≤ numcells) (hf : n < fuel + numcells) : specLeaves G tcLevel (fuel + extra) level lab ptn active numcells = specLeaves G tcLevel fuel level lab ptn active numcells

Every larger recursion bound enumerates exactly the same complete tree.