theorem
Hex.GraphIso.Nauty.Sparse.CountPartition.cell_iff
{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 first (last + 1 - first))
(ha : first ≤ a)
(hlen : 0 < len)
(hb : a + len ≤ last + 1)
:
Within an original cell, a new cell consists of one maximal run of equal counts. The two ends use the original boundaries or a count change.
theorem
Hex.GraphIso.Nauty.Sparse.CountPartition.nesting
{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 first (last + 1 - first))
(ho : IsCell ptn level a len)
:
A count split only subdivides its original cell. Every output cell is before it, after it, or contained in it.
theorem
Hex.GraphIso.Nauty.Sparse.CountPartition.cell_outside
{level first last : Nat}
{lab hits before ptn : Array Nat}
{a len : Nat}
(h : CountPartition level first last lab hits before ptn)
(hc : IsCell ptn level a len)
(hd : a + len ≤ first ∨ last < a)
:
IsCell before level a len
Cells outside the split retain their original partition data.
theorem
Hex.GraphIso.Nauty.Sparse.splitCounts_cell_iff
{n a len : 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)
(ha : first ≤ a)
(hlen : 0 < len)
(he : a + len ≤ s.cellend[first]! + 1)
:
have lab := (splitCounts level first distance s).lab;
IsCell (splitCounts level first distance s).ptn level a len ↔ (a = first ∨ s.hits[lab[a - 1]!]! ≠ s.hits[lab[a]!]!) ∧ (∀ (q : Nat), a ≤ q → q < a + len → s.hits[lab[q]!]! = s.hits[lab[a]!]!) ∧ (a + len - 1 = s.cellend[first]! ∨ s.hits[lab[a + len - 1]!]! ≠ s.hits[lab[a + len]!]!)
The actual count splitter's cells are exactly the maximal equal-count runs inside the incoming cell.