structure Hex.GraphIso.Nauty.Sparse.Minima.Bounded (lab hits : Array Nat) (first last v2 v3 upto w1 w2 cap : Nat) extends Hex.GraphIso.Nauty.Sparse.Minima lab hits first v2 v3 upto w1 w2 : Prop

Count insertion also retains the local key bound and the second-minimum sentinel. Values outside this cell remain unrestricted.

• bounds : first < v2 ∧ v2 ≤ v3 ∧ v3 ≤ upto
• keys : w1 < w2
• minimum (q : Nat) : first ≤ q → q < v2 → hits[lab[q]!]! = w1
• second (q : Nat) : v2 ≤ q → q < v3 → hits[lab[q]!]! = w2
• larger (q : Nat) : v3 ≤ q → q < upto → w2 < hits[lab[q]!]!
• size : last ≤ lab.size
• scan : upto ≤ last
• values (q : Nat) : first ≤ q → q < last → hits[lab[q]!]! < cap
• empty : v2 = v3 → w2 = cap

theorem Hex.GraphIso.Nauty.Sparse.Minima.Bounded.positions {lab hits : Array Nat} {first last v2 v3 upto w1 w2 cap : Nat} (h : Bounded lab hits first last v2 v3 upto w1 w2 cap) : first < v2 ∧ v2 ≤ v3 ∧ v3 ≤ upto

theorem Hex.GraphIso.Nauty.Sparse.Minima.Bounded.initial {lab hits : Array Nat} {first last upto w1 cap : Nat} (hb : first < upto) (hu : upto ≤ last) (hs : last ≤ lab.size) (hv : ∀ (q : Nat), first ≤ q → q < last → hits[lab[q]!]! < cap) (hm : ∀ (q : Nat), first ≤ q → q < upto → hits[lab[q]!]! = w1) : Bounded lab hits first last upto upto upto w1 cap cap

theorem Hex.GraphIso.Nauty.Sparse.Minima.Bounded.hit_min {lab hits : Array Nat} {first last v2 v3 upto w1 w2 cap : Nat} (h : Bounded lab hits first last v2 v3 upto w1 w2 cap) (hu : upto < last) (hk : hits[lab[upto]!]! = w1) : Bounded (((lab.set! upto lab[v3]!).set! v3 lab[v2]!).set! v2 lab[upto]!) hits first last (v2 + 1) (v3 + 1) (upto + 1) w1 w2 cap

theorem Hex.GraphIso.Nauty.Sparse.Minima.Bounded.hit_second {lab hits : Array Nat} {first last v2 v3 upto w1 w2 cap : Nat} (h : Bounded lab hits first last v2 v3 upto w1 w2 cap) (hu : upto < last) (hk : hits[lab[upto]!]! = w2) : Bounded ((lab.set! upto lab[v3]!).set! v3 lab[upto]!) hits first last v2 (v3 + 1) (upto + 1) w1 w2 cap

theorem Hex.GraphIso.Nauty.Sparse.Minima.Bounded.new_min {lab hits : Array Nat} {first last v2 v3 upto w1 w2 cap : Nat} (h : Bounded lab hits first last v2 v3 upto w1 w2 cap) (hu : upto < last) (hk : hits[lab[upto]!]! < w1) : Bounded (((lab.set! upto lab[v2]!).set! v2 lab[first]!).set! first lab[upto]!) hits first last (first + 1) (v2 + 1) (upto + 1) hits[lab[upto]!]! w1 cap

theorem Hex.GraphIso.Nauty.Sparse.Minima.Bounded.new_second {lab hits : Array Nat} {first last v2 v3 upto w1 w2 cap : Nat} (h : Bounded lab hits first last v2 v3 upto w1 w2 cap) (hu : upto < last) (hlo : w1 < hits[lab[upto]!]!) (hhi : hits[lab[upto]!]! < w2) : Bounded ((lab.set! upto lab[v2]!).set! v2 lab[upto]!) hits first last v2 (v2 + 1) (upto + 1) w1 hits[lab[upto]!]! cap

theorem Hex.GraphIso.Nauty.Sparse.Minima.Bounded.above {lab hits : Array Nat} {first last v2 v3 upto w1 w2 cap : Nat} (h : Bounded lab hits first last v2 v3 upto w1 w2 cap) (hu : upto < last) (hk : w2 < hits[lab[upto]!]!) : Bounded lab hits first last v2 v3 (upto + 1) w1 w2 cap

theorem Hex.GraphIso.Nauty.Sparse.Minima.Bounded.second_pos {lab hits : Array Nat} {first last v2 v3 w1 w2 cap : Nat} (h : Bounded lab hits first last v2 v3 last w1 w2 cap) (hv : v2 < last) : v2 < v3

Once the whole cell is scanned, a nonconstant split has two nonempty minimum fragments. The proof uses only this cell's bound, even when scratch entries belonging to other cells have arbitrary values.