theorem Hex.GraphIso.Nauty.Sparse.CountSort.finish_active {n : Nat} (level first last : Nat) (distance : Bool) (s : RefineSt n) (w1 v2 w2 v3 : Nat) (hb : last ≤ n) (hc : IsCell s.ptn level first (last - first)) (hm : Minima.Bounded s.lab s.hits first last v2 v3 last w1 w2 (n + 2)) : have t := finish level first last distance s w1 v2 w2 v3; CellActive level first last s.active t.active t.ptn ∧ ∀ (u : Nat), u < first ∨ last ≤ u → t.active.mem u = s.active.mem u

Fragment installation activates all fragments of an active cell and at most omits one otherwise. Replacement retains exterior membership.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_active {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hl : s.lab.size = n) (hb : s.cellend[first]! < n) (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) : have t := splitCounts level first distance s; CellActive level first (s.cellend[first]! + 1) s.active t.active t.ptn ∧ ∀ (u : Nat), u < first ∨ s.cellend[first]! + 1 ≤ u → t.active.mem u = s.active.mem u

Count splitting activates all fragments of an active cell and leaves at most one inactive fragment otherwise, preserving exterior membership.