Finite specifications for the native distinct-position frontend

The mathematical sets are the existing ThreeSum.splitA, ThreeSum.splitB, ThreeSum.twiceSet and ThreeSum.zeroSet. Native keys remain in unsigned encoding order. The specifications here describe compact subsequences of the radix key/count arrays.

Main definitions

• label: compute the shifted label from a canonical signed key.
• twice: the canonical key of twice the represented integer.
• select: compact selections from full key/count pairs.

Main results

• label_encode: native label arithmetic agrees with the existing mathematical label.
• twice_encode: doubling has the required positive sign.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.label (U u : ℕ) : ℕ

Shift a sign-and-magnitude key into the nonnegative label interval.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.twice (u : ℕ) : ℕ

The canonical key for twice the integer represented by a canonical key.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.flag (a b v mode : ℕ) (p : ℕ × ℕ) : Bool

A mode selects A, B₀, B₁, repeated nonzero values, repeated zero, or all values. Mode six is reserved for the separately written constant singleton zero.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.keep (U β β' v mode : ℕ) (p : ℕ × ℕ) : Bool

Selection from the two native label digits.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.value (mode u : ℕ) : ℕ

Key transformation after selection; only the repeated-nonzero mode doubles values.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.select (U β β' v mode : ℕ) (rs : List (ℕ × ℕ)) : List ℕ

Compact output of one native scan. Multiplicities are never truncated.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.length_select_le (U β β' v mode : ℕ) (rs : List (ℕ × ℕ)) : (select U β β' v mode rs).length ≤ rs.length

A single scan writes at most one cell per key/count pair.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.label_encode {U : ℕ} {z : ℤ} (hz : |z| ≤ ↑U) : label U (WordRAM.Signed.encode z) = ThreeSum.lab (2 * U) z

Native label arithmetic, including the absence of subtraction underflow.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.twice_encode (z : ℤ) : twice (WordRAM.Signed.encode z) = WordRAM.Signed.encode (2 * z)

The transient unsigned double is corrected by its low sign bit.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.key_bounds {U : ℕ} {z : ℤ} (hz : |z| ≤ ↑U) : WordRAM.Signed.encode z ≤ 2 * U + 1 ∧ label U (WordRAM.Signed.encode z) ≤ 3 * U ∧ WordRAM.Signed.encode z / 2 ≤ 2 * U ∧ 2 * WordRAM.Signed.encode z ≤ 4 * U + 2

Label arithmetic and the transient double stay within a common explicit bound.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.twice_injective : Function.Injective twice

The unsigned transformation is injective, even before restricting to canonical keys.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.value_injective (mode : ℕ) : Function.Injective (value mode)

Every output value transformation preserves injectivity.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.select_nodup (U β β' v mode : ℕ) {rs : List (ℕ × ℕ)} (h : (List.map Prod.fst rs).Nodup) : (select U β β' v mode rs).Nodup

Every compact scan enumerates its output without repetitions.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.mem_runs {input : List ℤ} {rs : List (ℕ × ℕ)} (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (hcounts : ∀ p ∈ rs, List.count p.1 (List.map WordRAM.Signed.encode input) = p.2) (p : ℕ × ℕ) : p ∈ rs ↔ ∃ z ∈ input, p = (WordRAM.Signed.encode z, List.count z input)

The supplied radix contracts identify every run with its exact input multiplicity.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.select_decoded {input : List ℤ} {rs : List (ℕ × ℕ)} (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (hcounts : ∀ p ∈ rs, List.count p.1 (List.map WordRAM.Signed.encode input) = p.2) (U β β' v mode : ℕ) : (List.map WordRAM.Signed.decode (select U β β' v mode rs)).toFinset = Finset.image (fun (z : ℤ) => WordRAM.Signed.decode (value mode (WordRAM.Signed.encode z))) ({z ∈ input.toFinset | keep U β β' v mode (WordRAM.Signed.encode z, List.count z input) = true})

A compact native selection represents precisely its finite filtered image.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.count_positions (input : List ℤ) (z : ℤ) : {i : Fin input.length | input[i] = z}.card = List.count z input

List multiplicity is exactly the number of original input positions.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.input_values (input : List ℤ) : Finset.image (fun (i : Fin input.length) => input[i]) Finset.univ = input.toFinset

Original input values are precisely the image of its positions.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.digit_eq (u β : ℕ) (v : Bool) : u >>> β % 2 = v.toNat ↔ u.testBit β = v

Native division/shift digits agree with the existing Boolean bit operation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.encode_eq_zero (z : ℤ) : WordRAM.Signed.encode z = 0 ↔ z = 0

Zero has exactly one canonical key.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.select_twice {input : List ℤ} {rs : List (ℕ × ℕ)} (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (hcounts : ∀ p ∈ rs, List.count p.1 (List.map WordRAM.Signed.encode input) = p.2) (U β β' v : ℕ) : (List.map WordRAM.Signed.decode (select U β β' v 3 rs)).toFinset = ThreeSum.twiceSet fun (i : Fin input.length) => input[i]

Exact bridge from the repeated-nonzero native scan to the existing twiceSet.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.select_original {input : List ℤ} {rs : List (ℕ × ℕ)} (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (hcounts : ∀ p ∈ rs, List.count p.1 (List.map WordRAM.Signed.encode input) = p.2) (U β β' v : ℕ) : (List.map WordRAM.Signed.decode (select U β β' v 5 rs)).toFinset = Finset.image (fun (i : Fin input.length) => input[i]) Finset.univ

The original-set scan preserves every distinct input value.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.select_zero {input : List ℤ} {rs : List (ℕ × ℕ)} (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (hcounts : ∀ p ∈ rs, List.count p.1 (List.map WordRAM.Signed.encode input) = p.2) (U β β' v : ℕ) : (List.map WordRAM.Signed.decode (select U β β' v 4 rs)).toFinset = ThreeSum.zeroSet fun (i : Fin input.length) => input[i]

The zero scan uses the full original multiplicity and threshold three.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.select_A {input : List ℤ} {rs : List (ℕ × ℕ)} {U : ℕ} (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (hcounts : ∀ p ∈ rs, List.count p.1 (List.map WordRAM.Signed.encode input) = p.2) (hvalues : ∀ z ∈ input, |z| ≤ ↑U) (β β' : ℕ) (v : Bool) : (List.map WordRAM.Signed.decode (select U β β' v.toNat 0 rs)).toFinset = ThreeSum.splitA (2 * U) β v (Finset.image (fun (i : Fin input.length) => input[i]) Finset.univ)

The A scan represents the exact existing bit split.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Math.select_B {input : List ℤ} {rs : List (ℕ × ℕ)} {U : ℕ} (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (hcounts : ∀ p ∈ rs, List.count p.1 (List.map WordRAM.Signed.encode input) = p.2) (hvalues : ∀ z ∈ input, |z| ≤ ↑U) (β β' : ℕ) (v w : Bool) : (List.map WordRAM.Signed.decode (select U β β' v.toNat (if w = true then 2 else 1) rs)).toFinset = ThreeSum.splitB (2 * U) β β' v w (Finset.image (fun (i : Fin input.length) => input[i]) Finset.univ)

Both B scans represent the exact existing two-bit split, including β=β'.