theorem Hex.GraphIso.Nauty.Sparse.Minima.unique {keys lab hits : Array Nat} {first v2 v3 last w1 w2 : Nat} {out : Array Nat} {u2 u3 z1 z2 : Nat} (h : Minima lab hits first v2 v3 last w1 w2) (h' : Minima out keys first u2 u3 last z1 z2) (hv : v2 < v3) (hu : u2 < u3) (hk : ∀ (q : Nat), first ≤ q → q < last → hits[lab[q]!]! = keys[out[q]!]!) : w1 = z1 ∧ v2 = u2 ∧ w2 = z2 ∧ v3 = u3

The first two runs determine their minimum keys and cut positions. The nonempty second run is the branch used after a nonuniform cell scan.

theorem Hex.GraphIso.Nauty.Sparse.Minima.data_eq {keys lab hits : Array Nat} {first v2 v3 last w1 w2 : Nat} {out : Array Nat} {u2 u3 z1 z2 : Nat} (h : Minima lab hits first v2 v3 last w1 w2) (h' : Minima out keys first u2 u3 last z1 z2) (hb : last ≤ lab.size) (hb' : last ≤ out.size) (hv : v2 < v3) (hu : u2 < u3) (hp : (List.map (fun (v : Nat) => hits[v]!) (segN lab first (last - first))).Perm (List.map (fun (v : Nat) => keys[v]!) (segN out first (last - first)))) : w1 = z1 ∧ v2 = u2 ∧ w2 = z2 ∧ v3 = u3

Permuting the input count multiset cannot change the two minimum keys or either cutoff found by the executed insertion. Sorting the tail is used only in this proof to compare the two completed invariants.

theorem Hex.GraphIso.Nauty.Sparse.Minima.Permuted.constant {before lab hits : Array Nat} {first last v2 v3 w1 w2 cap q : Nat} (h : Permuted before lab hits first last v2 v3 last w1 w2 cap) (he : v2 = last) (hq : first ≤ q) (hb : q < last) : hits[before[q]!]! = hits[before[first]!]!

A one-class insertion result implies that the original cell was uniform. This rules out the redundant late uniform-return guard after the first unequal input count has been found.