theorem Hex.GraphIso.Nauty.Sparse.Binary.cut_congr {first last : Nat} {lab other : Array Nat} {pred test : Nat → Bool} (hl : other = lab) (hk : ∀ (v : Nat), v ∈ seen lab first last → test v = pred v) : cut other test first last = cut lab pred first last

The compaction cut depends only on the input labels and observed predicate, rather than on the retained mark values or generation number.

theorem Hex.GraphIso.Nauty.Sparse.Binary.Cell.ptn_eq {n level first last : Nat} {pred other : Nat → Bool} {s t a b : RefineSt n} (hs : Cell level first last pred s a) (ht : Cell level first last other t b) (hl : t.lab = s.lab) (hp : t.ptn = s.ptn) (hk : ∀ (v : Nat), v ∈ seen s.lab first last → other v = pred v) : a.ptn = b.ptn

Equal inputs and observed marks close precisely the same boundary.

theorem Hex.GraphIso.Nauty.Sparse.Binary.Cell.lab_eq {n level first last : Nat} {pred other : Nat → Bool} {s t a b : RefineSt n} (hs : Cell level first last pred s a) (ht : Cell level first last other t b) (hl : t.lab = s.lab) (hf : first ≤ last) (hk : ∀ (v : Nat), v ∈ seen s.lab first last → other v = pred v) : a.lab = b.lab

Identical singleton-cell input orders and mark predicates give identical output arrays. Retained marks outside this cell and the numeric generation need not agree.