structure Hex.GraphIso.Nauty.Sparse.CountPartition (level first upto : Nat) (lab hits before ptn : Array Nat) : Prop

The processed boundary positions split exactly at a change of count. Positions outside that prefix retain their original partition values.

• size : ptn.size = before.size
• head (q : Nat) : q < first → ptn[q]! = before[q]!
• cuts (q : Nat) : first ≤ q → q < upto → ptn[q]! = if hits[lab[q]!]! = hits[lab[q + 1]!]! then before[q]! else level
• tail (q : Nat) : upto ≤ q → ptn[q]! = before[q]!

theorem Hex.GraphIso.Nauty.Sparse.CountPartition.constant {first upto : Nat} {hits lab : Array Nat} {value level : Nat} {ptn : Array Nat} (h : ∀ (q : Nat), first ≤ q → q ≤ upto → hits[lab[q]!]! = value) : CountPartition level first upto lab hits ptn ptn

theorem Hex.GraphIso.Nauty.Sparse.CountPartition.equal {level first upto : Nat} {lab hits before ptn : Array Nat} (h : CountPartition level first upto lab hits before ptn) (he : hits[lab[upto]!]! = hits[lab[upto + 1]!]!) : CountPartition level first (upto + 1) lab hits before ptn

theorem Hex.GraphIso.Nauty.Sparse.CountPartition.different {level first upto : Nat} {lab hits before ptn : Array Nat} (h : CountPartition level first upto lab hits before ptn) (hl : first ≤ upto) (hb : upto < before.size) (he : hits[lab[upto]!]! ≠ hits[lab[upto + 1]!]!) : CountPartition level first (upto + 1) lab hits before (ptn.setIfInBounds upto level)

theorem Hex.GraphIso.Nauty.Sparse.CountPartition.minima {lab hits : Array Nat} {first v2 v3 last w1 w2 level : Nat} {ptn : Array Nat} (h : Minima lab hits first v2 v3 last w1 w2) (hv : v2 < v3) (hb : v2 - 1 < ptn.size) : CountPartition level first (v3 - 1) lab hits ptn (ptn.setIfInBounds (v2 - 1) level)

The first two nonempty minimum fragments need exactly one new boundary.

theorem Hex.GraphIso.Nauty.Sparse.Minima.indirect {lab hits : Array Nat} {first v2 v3 last w1 w2 : Nat} (h : Minima lab hits first v2 v3 last w1 w2) (hb : last ≤ lab.size) : Minima («Sort».indirect lab hits v3 (last - v3)) hits first v2 v3 last w1 w2

Sorting the larger-count tail retains both minimum fragments and their strict separation from the tail.

theorem Hex.GraphIso.Nauty.Sparse.Minima.next_different {lab hits : Array Nat} {first v2 v3 last w1 w2 : Nat} (h : Minima lab hits first v2 v3 last w1 w2) (hv : v2 < v3) (ht : v3 < last) : hits[lab[v3 - 1]!]! ≠ hits[lab[v3 - 1 + 1]!]!