theorem Hex.GraphIso.Nauty.Sparse.Refinement.queue_scan {n : Nat} (active : VSet n) : ActiveScan active (queue active) none

The literal packed active scan exhausts its bounded queue enumeration.

theorem Hex.GraphIso.Nauty.Sparse.Refinement.initial_valid {n : Nat} (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (scratch : Scratch) (hp : lab.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (ha : ∀ (v : Nat), active.mem v = true → v = 0 ∨ ptn[v - 1]! ≤ level) (hb : Scratch.Bounded n scratch) : RefineSt.Valid level (indexed level (start lab ptn active numcells scratch))

Index rebuilding establishes a valid working state from any bounded scratch, regardless of its old cache flag and contents.

theorem Hex.GraphIso.Nauty.Sparse.Refinement.initial_equiv {n : Nat} (σ : Renaming n) (level : Nat) (lab out ptn : Array Nat) (active : VSet n) (numcells : Nat) (s t : Scratch) (hc : cellsPerm ptn level out (Array.map σ.toFun lab)) : RefineSt.Equiv σ level (indexed level (start lab ptn active numcells s)) (indexed level (start out ptn active numcells t))

Initial observations depend on cell contents and the supplied count, independently of rebuilt index representations and scratch contents.

theorem Hex.GraphIso.Nauty.Sparse.Refinement.finish_equiv {n : Nat} {σ : Renaming n} {level : Nat} {s t : RefineSt n} (h : RefineSt.Equiv σ level s t) : RefineSt.Equiv σ level (finish s) (finish t)

The literal final hash cleanup preserves observation equivalence.