theorem Hex.GraphIso.Nauty.Sparse.splitCounts_cuts {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hl : s.lab.size = n) (hs : s.ptn.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) : Cuts level n s.ptn (splitCounts level first distance s).ptn s.numcells (splitCounts level first distance s).numcells n

Every increment of the executed count splitter's cell counter corresponds exactly to a newly closed partition boundary. Scratch counts are bounded only on the cell being divided, and old closed boundary values are retained.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_count {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hl : s.lab.size = n) (hs : s.ptn.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) : bcount (splitCounts level first distance s).ptn level n + s.numcells = bcount s.ptn level n + (splitCounts level first distance s).numcells

The counter increment is exactly the number of newly closed boundaries.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_closed {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hl : s.lab.size = n) (hs : s.ptn.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) (q : Nat) (hq : s.ptn[q]! ≤ level) : (splitCounts level first distance s).ptn[q]! = s.ptn[q]!

Closed partition values, including boundaries inherited from ancestors, are retained literally by the count splitter.