theorem
Hex.GraphIso.Nauty.Sparse.CountSort.finish_cuts
{n : Nat}
(level first last : Nat)
(distance : Bool)
(s : RefineSt n)
(w1 v2 w2 v3 : Nat)
(hs : s.ptn.size = n)
(hb : last ≤ n)
(hm : Minima.Bounded s.lab s.hits first last v2 v3 last w1 w2 (n + 2))
(hopen : ∀ (q : Nat), first ≤ q → q < last - 1 → level < s.ptn[q]!)
:
Fragment installation charges exactly one new cell to every boundary it closes, and retains all previously closed partition values.
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
Count splitting closes one boundary for every new partition cell.
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)
:
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)
:
Closed partition values, including boundaries inherited from ancestors, are retained literally by the count splitter.