Fixed-length radix arithmetic

These lemmas use Mathlib's Nat.ofDigits and finFunctionFinEquiv to relate fixed tuples of digits, exact carry equations, and ordinary natural-number values. No modular overflow is implicit in a carry equation.

Main definitions

• Cslib.Radix.digit: recursive fixed-position digit extraction.
• Cslib.Radix.pack: little-endian finite-tuple packing with a fixed enumeration.
• Cslib.Radix.component: extraction using the same finite-tuple enumeration.

Main results

• Nat.ofDigits_ofFn_eq_sum: fixed tuples have the usual weighted value.
• Nat.exists_ofDigits_ofFn: every value below the fixed capacity has bounded digits.
• Nat.radix_carry_split: one exact low-digit equation and its remaining carry.
• Cslib.Radix.component_pack, Cslib.Radix.pack_lt: recovery and capacity for tuples indexed by any fixed finite type, independently of a machine or resource model.
• finFunctionFinEquiv_snoc, finFunctionFinEquiv_eq_of_high_zero, finFunctionFinEquiv_lt_pow_iff, finFunctionFinEquiv_lt_iff: highest-digit splitting, zero high digits, power bounds, and colexicographic order for finFunctionFinEquiv.

References

The application to full-tuple numeric predicates follows [Imm99], Exercise 1.33(3).

theorem Nat.ofDigits_ofFn_succ {d : ℕ} (B : ℕ) (x : Fin (d + 1) → ℕ) : ofDigits B (List.ofFn x) = x 0 + B * ofDigits B (List.ofFn fun (i : Fin d) => x i.succ)

The value of d + 1 digits is the first digit plus B times the value of the remaining digits.

theorem Nat.ofDigits_ofFn_eq_sum {d : ℕ} (B : ℕ) (x : Fin d → ℕ) : ofDigits B (List.ofFn x) = ∑ i : Fin d, x i * B ^ ↑i

The value of a tuple x of digits in base B is ∑ i, x i * B ^ i.

theorem Nat.ofDigits_ofFn_lt {B d : ℕ} (hB : 1 < B) (x : Fin d → ℕ) (hx : ∀ (i : Fin d), x i < B) : ofDigits B (List.ofFn x) < B ^ d

For 1 < B, the value of d digits less than B is less than B ^ d.

theorem Nat.ofDigits_lt_base_pow_length_of_pos {B : ℕ} (_hB : 0 < B) (l : List ℕ) (hl : ∀ a ∈ l, a < B) : ofDigits B l < B ^ l.length

Bounded digits fit in their radix power, including radix one and the empty word.

theorem Nat.ofDigits_ofFn_inj {B d : ℕ} (hB : 1 < B) {x y : Fin d → ℕ} (hx : ∀ (i : Fin d), x i < B) (hy : ∀ (i : Fin d), y i < B) (h : ofDigits B (List.ofFn x) = ofDigits B (List.ofFn y)) : x = y

For 1 < B, two tuples of digits less than B with the same value are equal.

theorem Nat.exists_ofDigits_ofFn {B d v : ℕ} (hv : v < B ^ d) : ∃ (x : Fin d → ℕ), (∀ (i : Fin d), x i < B) ∧ ofDigits B (List.ofFn x) = v

Fixed-length digits exist for every fitting value, including the empty tuple at zero.

theorem Nat.ofDigits_ofFn_div_mod {B d : ℕ} (x : Fin d → ℕ) (hx : ∀ (i : Fin d), x i < B) (i : Fin d) : ofDigits B (List.ofFn x) / B ^ ↑i % B = x i

The digit at i of a tuple of digits less than B is recovered from its value v as v / B ^ i % B.

theorem Nat.ofDigits_eq_of_quotients {B d : ℕ} (x : Fin d → ℕ) (q : Fin (d + 1) → ℕ) (hq : q (Fin.last d) = 0) (hs : ∀ (i : Fin d), q i.castSucc = x i + B * q i.succ) : ofDigits B (List.ofFn x) = q 0

A zero-ended sequence of exact quotients decodes a word without ignoring high digits.

theorem Nat.exists_radix_quotients {B d : ℕ} (hB : 1 ≤ B) (x : Fin d → ℕ) : ∃ (q : Fin (d + 1) → ℕ), q 0 = ofDigits B (List.ofFn x) ∧ q (Fin.last d) = 0 ∧ (∀ (i : Fin (d + 1)), q i ≤ ofDigits B (List.ofFn x)) ∧ ∀ (i : Fin d), q i.castSucc = x i + B * q i.succ

All suffix quotients of a word are bounded by its whole value.

theorem Nat.testBit_ofDigits_ofFn {e d : ℕ} (he : 0 < e) (x : Fin d → ℕ) (hx : ∀ (i : Fin d), x i < 2 ^ e) (j : ℕ) : (ofDigits (2 ^ e) (List.ofFn x)).testBit j = true ↔ ∃ (r : Fin d) (b : Fin e), ↑r * e + ↑b = j ∧ (x r).testBit ↑b = true

A bit of a binary-radix word belongs to exactly one of its fixed chunks.

theorem Nat.radix_carry_split {B t u z v : ℕ} (hB : 0 < B) (hz : z < B) (h : t + B * u = z + B * v) : t = z + B * (t / B) ∧ u + t / B = v

An exact low-digit equation determines both the carry and the remaining value.

theorem Nat.radix_affine_carries_iff {B d b c₀ : ℕ} (hB : 1 < B) (hb : b ≤ B) (hc₀ : c₀ ≤ B) (x y z : Fin d → ℕ) (hx : ∀ (i : Fin d), x i < B) (hy : ∀ (i : Fin d), y i < B) (hz : ∀ (i : Fin d), z i < B) : (∃ (c : Fin (d + 1) → ℕ), c 0 = c₀ ∧ c (Fin.last d) = 0 ∧ (∀ (i : Fin (d + 1)), c i ≤ B) ∧ ∀ (i : Fin d), x i * b + y i + c i.castSucc = z i + B * c i.succ) ↔ b * ofDigits B (List.ofFn x) + ofDigits B (List.ofFn y) + c₀ = ofDigits B (List.ofFn z)

Bounded, zero-ended carries characterize multiplication by one digit plus another word.

theorem Nat.exists_binary_radix {n : ℕ} (hn : 8 < n) : ∃ (e : ℕ), 0 < e ∧ (2 ^ e) ^ 3 < n ∧ n < (2 ^ e) ^ 7

Every universe larger than eight admits binary digits whose products fit, while its cardinality itself fits in seven digits. The cardinality need not be a source element.

def Cslib.Radix.digit (B x : ℕ) : ℕ → ℕ

Read a digit by repeatedly dividing by the radix. This is total even at radix zero.

theorem Cslib.Radix.digit_eq_div_pow_mod (B x i : ℕ) : digit B x i = x / B ^ i % B

The recursive extractor agrees with ordinary fixed-position radix arithmetic.

theorem Cslib.Radix.digit_ofDigits {B : ℕ} (_hB : 0 < B) (l : List ℕ) (hl : ∀ a ∈ l, a < B) (i : ℕ) (hi : i < l.length) : digit B (Nat.ofDigits B l) i = l[i]

Recover a bounded digit of a little-endian word, including radix one.

noncomputable def Cslib.Radix.pack {ι : Type} [Fintype ι] (B : ℕ) (f : ι → ℕ) : ℕ

Pack a finite tuple in little-endian order using the fixed Fintype.equivFin enumeration. The enumeration is independent of the radix and tuple values.

noncomputable def Cslib.Radix.component {ι : Type} [Fintype ι] (B x : ℕ) (i : ι) : ℕ

Read one component using the same fixed enumeration as pack.

theorem Cslib.Radix.component_pack {ι : Type} [Fintype ι] {B : ℕ} (_hB : 0 < B) {f : ι → ℕ} (hf : ∀ (i : ι), f i < B) (i : ι) : component B (pack B f) i = f i

Bounded finite-tuple components are recovered exactly, including radix one.

theorem Cslib.Radix.pack_lt {ι : Type} [Fintype ι] {B : ℕ} (hB : 0 < B) {f : ι → ℕ} (hf : ∀ (i : ι), f i < B) : pack B f < B ^ Fintype.card ι

Bounded finite tuples fit below their radix power, including the empty tuple.

finFunctionFinEquiv order and prefix lemmas

theorem finFunctionFinEquiv_snoc {n k : ℕ} (x : Fin (k + 1) → Fin n) : ↑(finFunctionFinEquiv x) = ↑(finFunctionFinEquiv (x ∘ Fin.castSucc)) + ↑(x (Fin.last k)) * n ^ k

Separate the highest-weight digit (x (Fin.last k) : ℕ) * n ^ k of finFunctionFinEquiv x.

theorem finFunctionFinEquiv_eq_of_high_zero {n a k : ℕ} (ha : a ≤ k) {x : Fin k → Fin n} : (∀ (i : Fin k), a ≤ ↑i → ↑(x i) = 0) → ↑(finFunctionFinEquiv x) = ↑(finFunctionFinEquiv fun (j : Fin a) => x (Fin.castLE ha j))

When all coordinates of x : Fin k → Fin n at indices ≥ a are zero, finFunctionFinEquiv x has the same value as its prefix of length a.

theorem finFunctionFinEquiv_lt_pow_iff {n a k : ℕ} : a ≤ k → ∀ (x : Fin k → Fin n), ↑(finFunctionFinEquiv x) < n ^ a ↔ ∀ (i : Fin k), a ≤ ↑i → ↑(x i) = 0

For a ≤ k, a k-tuple has finFunctionFinEquiv value < n ^ a iff all coordinates at indices ≥ a are zero.

theorem finFunctionFinEquiv_lt_iff {n k : ℕ} (x y : Fin k → Fin n) : finFunctionFinEquiv x < finFunctionFinEquiv y ↔ ∃ (i : Fin k), x i < y i ∧ ∀ (j : Fin k), i < j → x j = y j

The numerical order on finFunctionFinEquiv is the colexicographic order on Fin k → Fin n (comparing at the most significant coordinate where the tuples differ).