theorem Hex.GraphIso.Nauty.Sparse.CountSort.firstRun_bounds (lab hits : Array Nat) (first last : Nat) (hf : first < last) : first < firstRun lab hits first last ∧ firstRun lab hits first last ≤ last

The initial equal-count scan stops inside the cell or at its exclusive end.

theorem Hex.GraphIso.Nauty.Sparse.CountSort.firstRun_spec (lab hits : Array Nat) (first last : Nat) (hf : first < last) : have v := firstRun lab hits first last; first < v ∧ v ≤ last ∧ (∀ (q : Nat), first ≤ q → q < v → hits[lab[q]!]! = hits[lab[first]!]!) ∧ (v = last ∨ hits[lab[v]!]! ≠ hits[lab[first]!]!)

The initial scan records a constant prefix and stops at its first unequal count, or exhausts the cell.

theorem Hex.GraphIso.Nauty.Sparse.CountSort.minima_window (lab hits : Array Nat) (cap first last begin : Nat) (hf : first < begin) (he : begin ≤ last) (hb : last ≤ lab.size) : have r := minima lab hits cap first last begin; «Sort».Window lab r.snd.snd.snd.snd first last ∧ first < r.snd.fst ∧ r.snd.fst ≤ r.snd.snd.snd.fst ∧ r.snd.snd.snd.fst ≤ last

Three-way insertion permutes only the selected cell and leaves ordered, bounded fragment cuts. It does not require bounds on the count values.

theorem Hex.GraphIso.Nauty.Sparse.CountSort.minima_spec (lab hits : Array Nat) (cap first last begin : Nat) (hf : first < begin) (he : begin ≤ last) (hb : last ≤ lab.size) (hk : hits[lab[first]!]! < cap) (hu : ∀ (q : Nat), first ≤ q → q < begin → hits[lab[q]!]! = hits[lab[first]!]!) : have r := minima lab hits cap first last begin; Minima r.snd.snd.snd.snd hits first r.snd.fst r.snd.snd.snd.fst last r.fst r.snd.snd.fst ∧ r.snd.snd.snd.snd.size = lab.size

Three-way insertion leaves the two minimum-count runs followed by strictly larger counts. The sentinel need only exceed the initial count.