theorem Hex.GraphIso.Nauty.Sparse.Compact.produceNode_replays {n : Nat} {G : SparseGraph n} {tcLevel fuel level numcells : Nat} {gens : List (Perm n)} {lab ptn : Array Nat} {active : VSet n} {B : Key n} (hp : lab.toList.Perm (List.range n)) (ho : NodeOk n level lab ptn active) (hc : numcells = bcount ptn level n) (hl : level ≤ numcells) (hf : n < fuel + numcells) (hb : ∀ (l : SpecLeaf n), l ∈ specLeaves G tcLevel fuel level lab ptn active numcells → (SpecLeaf.key G l).Le B) : ∃ (a : Bool), checkNode G tcLevel fuel level lab ptn active numcells (produceNode G tcLevel gens fuel level lab ptn active numcells B) B = some a

Unlimited compact production succeeds against every genuine upper bound. The generator list may be arbitrary: proposals are checked before emission, and unavailable or rejected witnesses retain full recursive expansion.