theorem Hex.GraphIso.Nauty.Sparse.Sort.get_swap (x : Array Nat) (i j q : Nat) (hi : i < x.size) (hj : j < x.size) (hq : q < x.size) : (x.swapIfInBounds i j)[q]! = if q = i then x[j]! else if q = j then x[i]! else x[q]!

structure Hex.GraphIso.Nauty.Sparse.Sort.Cuts (x y : Array Nat) (lo hi v a b c d : Nat) : Prop

The four processed regions around the unscanned interval [b,c). The equal-pivot regions remain at the two ends until the final block swaps.

• bounds : lo ≤ a ∧ a ≤ b ∧ b ≤ c ∧ c ≤ d ∧ d ≤ hi
• left_eq (q : Nat) : lo ≤ q → q < a → y[x[q]!]! = v
• left_lt (q : Nat) : a ≤ q → q < b → y[x[q]!]! < v
• right_gt (q : Nat) : c ≤ q → q < d → v < y[x[q]!]!
• right_eq (q : Nat) : d ≤ q → q < hi → y[x[q]!]! = v

theorem Hex.GraphIso.Nauty.Sparse.Sort.Cuts.initial (x y : Array Nat) (lo hi v : Nat) (h : lo ≤ hi) : Cuts x y lo hi v lo lo hi hi

theorem Hex.GraphIso.Nauty.Sparse.Sort.Cuts.left_lt_step {x y : Array Nat} {lo hi v a b c d : Nat} (h : Cuts x y lo hi v a b c d) (hbc : b < c) (hk : y[x[b]!]! < v) : Cuts x y lo hi v a (b + 1) c d

theorem Hex.GraphIso.Nauty.Sparse.Sort.Cuts.right_gt_step {x y : Array Nat} {lo hi v a b c d : Nat} (h : Cuts x y lo hi v a b c d) (hbc : b < c) (hk : v < y[x[c - 1]!]!) : Cuts x y lo hi v a b (c - 1) d

theorem Hex.GraphIso.Nauty.Sparse.Sort.Cuts.left_eq_step {x y : Array Nat} {lo hi v a b c d : Nat} (h : Cuts x y lo hi v a b c d) (hs : hi ≤ x.size) (hbc : b < c) (hk : y[x[b]!]! = v) : Cuts (x.swapIfInBounds a b) y lo hi v (a + 1) (b + 1) c d

theorem Hex.GraphIso.Nauty.Sparse.Sort.Cuts.right_eq_step {x y : Array Nat} {lo hi v a b c d : Nat} (h : Cuts x y lo hi v a b c d) (hs : hi ≤ x.size) (hbc : b < c) (hk : y[x[c - 1]!]! = v) : Cuts (x.swapIfInBounds (c - 1) (d - 1)) y lo hi v a b (c - 1) (d - 1)

theorem Hex.GraphIso.Nauty.Sparse.Sort.Cuts.cross {x y : Array Nat} {lo hi v a b c d : Nat} (h : Cuts x y lo hi v a b c d) (hs : hi ≤ x.size) (hbc : b < c) (hl : v < y[x[b]!]!) (hr : y[x[c - 1]!]! < v) : Cuts (x.swapIfInBounds b (c - 1)) y lo hi v a (b + 1) (c - 1) d

structure Hex.GraphIso.Nauty.Sparse.Sort.Store (x base y : Array Nat) (lo hi v : Nat) : Prop

Allocation, exterior entries, and an occurrence of the sampled pivot are preserved by every partition swap.

• size_eq : x.size = base.size
• outside (q : Nat) : q < lo ∨ hi ≤ q → x[q]! = base[q]!
• seen : ∃ (q : Nat), lo ≤ q ∧ q < hi ∧ y[x[q]!]! = v

theorem Hex.GraphIso.Nauty.Sparse.Sort.Store.swap {x base y : Array Nat} {lo hi v i j : Nat} (h : Store x base y lo hi v) (hs : hi ≤ x.size) (hib : lo ≤ i ∧ i < hi) (hj : lo ≤ j ∧ j < hi) : Store (x.swapIfInBounds i j) base y lo hi v

theorem Hex.GraphIso.Nauty.Sparse.Sort.Cuts.proper {x base y : Array Nat} {lo hi v a b c d : Nat} (h : Cuts x y lo hi v a b c d) (hs : Store x base y lo hi v) : b - a + (d - c) < hi - lo

The two recursive fragments omit at least one pivot occurrence.

theorem Hex.GraphIso.Nauty.Sparse.Sort.right_stop (x y : Array Nat) (b c d v : Nat) (hbc : b < c) (hcd : c ≤ d) (hs : d ≤ x.size) (h : b = c ∨ v < y[x[b]!]!) : b = c - 1 ∨ v < y[(x.swapIfInBounds (c - 1) (d - 1))[b]!]!

The right scan preserves the left scan's stopping condition.

theorem Hex.GraphIso.Nauty.Sparse.Sort.partition_proper (x y : Array Nat) (start len : Nat) (hb : start + len ≤ x.size) (hl : 0 < len) : (partition x y start len).snd.fst + (partition x y start len).snd.snd < len ∧ ∀ (q : Nat), q < start ∨ start + len ≤ q → (partition x y start len).fst[q]! = x[q]!

The recursive fragments exclude a pivot entry, and all swaps stay inside the requested segment.