Stable counting-sort positions

Main definitions

• CountingSort.position: stable scatter position of an original occurrence.

Main results

• CountingSort.count_lt_succ: the prefix-sum update used by a native counting pass.
• CountingSort.position_injective: every original position has a distinct destination.
• CountingSort.position_bijective: scatter destinations form a permutation of the input.
• CountingSort.scatter_span_image: an actual scattered array's bucket span has exactly the values whose original keys select that bucket.

These finite counting identities are original supporting mathematics for the native router. They reuse Mathlib's Nat.count and its prefix-count APIs directly; only the stable-scatter construction and cross-bucket theory are added. They assert no program or execution cost.

def Cslib.Algorithms.CountingSort.position (key : ℕ → ℕ) (n i : ℕ) : ℕ

The stable destination of original position i in an input of length n.

theorem Cslib.Algorithms.CountingSort.count_lt_succ (key : ℕ → ℕ) (n b : ℕ) : Nat.count (fun (k : ℕ) => key k < b + 1) n = Nat.count (fun (k : ℕ) => key k < b) n + Nat.count (fun (k : ℕ) => key k = b) n

One prefix-sum step appends exactly the current bucket's cardinality.

theorem Cslib.Algorithms.CountingSort.position_mem (key : ℕ → ℕ) {n i : ℕ} (hi : i < n) : Nat.count (fun (k : ℕ) => key k < key i) n ≤ position key n i ∧ position key n i < Nat.count (fun (k : ℕ) => key k < key i + 1) n

Each occurrence lands before the next bucket, and after its own bucket's start.

theorem Cslib.Algorithms.CountingSort.position_lt (key : ℕ → ℕ) {n i : ℕ} (hi : i < n) : position key n i < n

Stable scatter destinations are valid original-length indices.

theorem Cslib.Algorithms.CountingSort.position_lt_same (key : ℕ → ℕ) (n : ℕ) {i j : ℕ} (hij : i < j) (hkey : key i = key j) : position key n i < position key n j

Original order is retained inside a bucket.

theorem Cslib.Algorithms.CountingSort.position_lt_key (key : ℕ → ℕ) {n i j : ℕ} (hi : i < n) (hkey : key i < key j) : position key n i < position key n j

Every position in a smaller bucket precedes every position in a larger bucket.

theorem Cslib.Algorithms.CountingSort.position_injective (key : ℕ → ℕ) (n : ℕ) : Function.Injective fun (i : Fin n) => position key n ↑i

Distinct original positions never overwrite one another during stable scatter.

theorem Cslib.Algorithms.CountingSort.position_bijective (key : ℕ → ℕ) (n : ℕ) : Function.Bijective fun (i : Fin n) => ⟨position key n ↑i, ⋯⟩

All original occurrences, including equal keys, are a permutation of the output cells.

theorem Cslib.Algorithms.CountingSort.position_mem_iff (key : ℕ → ℕ) {n i : ℕ} (hi : i < n) (b : ℕ) : Nat.count (fun (k : ℕ) => key k < b) n ≤ position key n i ∧ position key n i < Nat.count (fun (k : ℕ) => key k < b + 1) n ↔ key i = b

A stable destination belongs to a bucket's half-open span exactly when its key is that bucket. Equal values or repeated original requests do not change the interval criterion.

theorem Cslib.Algorithms.CountingSort.scatter_span_image {α : Type u_1} [DecidableEq α] (key : ℕ → ℕ) (n b : ℕ) (stored values : ℕ → α) (h : ∀ i < n, stored (position key n i) = values i) : Finset.image stored (Finset.Ico (Nat.count (fun (k : ℕ) => key k < b) n) (Nat.count (fun (k : ℕ) => key k < b + 1) n)) = Finset.image values ({i ∈ Finset.range n | key i = b})

A memory array satisfying the stable-scatter equations has precisely the original values selected by each bucket. No sorted list or permutation certificate is a premise.