theorem
Hex.GraphIso.Nauty.Sparse.CountPartition.preserve
{level first last : Nat}
{lab hits before ptn : Array Nat}
{a len : Nat}
(h : CountPartition level first last lab hits before ptn)
(hc : IsCell before level a len)
(hd : a + len ≤ first ∨ last < a)
:
IsCell ptn level a len
A count split retains the full partition contract of a disjoint cell.
theorem
Hex.GraphIso.Nauty.Sparse.splitCounts_other
{n : Nat}
(level first a len limit : 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)
(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)
(ha : IsCell s.ptn level a len)
(hne : a ≠ first)
(hh : ∀ (q : Nat), a ≤ q → q < a + len → s.hits[s.lab[q]!]! ≤ limit)
:
Splitting one touched cell preserves the partition and local hit bound of every other pending cell.