theorem Hex.GraphIso.Nauty.Sparse.CountSort.finish_partition {n : Nat} (level first last : Nat) (distance : Bool) (s : RefineSt n) (w1 v2 w2 v3 : Nat) (hb : last ≤ s.ptn.size) (hm : Minima.Bounded s.lab s.hits first last v2 v3 last w1 w2 (n + 2)) : CountPartition level first (last - 1) (finish level first last distance s w1 v2 w2 v3).lab s.hits s.ptn (finish level first last distance s w1 v2 w2 v3).ptn

Fragment installation closes exactly the boundaries between unequal adjacent counts and preserves every other partition value.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_partition {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hl : s.lab.size = n) (hs : s.ptn.size = n) (hf : first ≤ s.cellend[first]!) (hb : s.cellend[first]! < n) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) : CountPartition level first s.cellend[first]! (splitCounts level first distance s).lab s.hits s.ptn (splitCounts level first distance s).ptn

Count splitting closes exactly the boundaries between unequal counts.