theorem Hex.GraphIso.Nauty.Sparse.Binary.cut_bounds {first last : Nat} (lab : Array Nat) (pred : Nat → Bool) (hf : first ≤ last) : first ≤ cut lab pred first last ∧ cut lab pred first last ≤ last

The compaction cut lies in its input interval, including empty classes.

theorem Hex.GraphIso.Nauty.Sparse.Binary.Cell.equiv {n level first last : Nat} {pred other : Nat → Bool} {s t a b : RefineSt n} (f : Nat → Nat) (hs : Cell level first last pred s a) (ht : Cell level first last other t b) (hsl : s.lab.size = n) (htl : t.lab.size = n) (hsp : s.ptn.size = n) (htp : t.ptn = s.ptn) (hb : last ≤ n) (hcell : IsCell s.ptn level first (last - first)) (hp : cellsPerm s.ptn level t.lab (Array.map f s.lab)) (hk : ∀ (v : Nat), v ∈ seen s.lab first last → other (f v) = pred v) (hcontrol : CountTrace.control s = CountTrace.control t) (hnum : s.numcells = t.numcells) : a.ptn = b.ptn ∧ cellsPerm a.ptn level b.lab (Array.map f a.lab) ∧ CountTrace.control a = CountTrace.control b ∧ a.numcells = b.numcells

Complete singleton-cell observations transport under a mapped input permutation and predicate. The updated partition's every cell, its literal control and the exact cell count agree.