Fixed-width binary encodings of natural numbers

Big-endian, fixed-width binary encoding Nat.toBits with its exact decoder Nat.fromBits, plus the little-endian views Nat.toBitsLE and Nat.fromBitsLE used by local Turing-machine arithmetic. Both conventions have exact length, truncation, round-trip, and fixed-width injectivity lemmas. Values wider than the target width are truncated modulo 2 ^ w.

This file lives in Complexitylib/Mathlib/ because it extends a Mathlib type in its home (root) namespace — the sanctioned exception to the Complexity root-namespace rule. Its contents are candidates for upstreaming to Mathlib.

def Nat.toBits : ℕ → ℕ → List Bool

Encode a natural number as a big-endian binary list of exactly w bits. Numbers larger than 2^w - 1 are truncated (mod 2^w).

Equations

• Nat.toBits 0 x✝ = []
• w.succ.toBits x✝ = (x✝ / 2 ^ w % 2 == 1) :: w.toBits x✝

theorem Nat.length_toBits (w val : ℕ) : (w.toBits val).length = w

def Nat.fromBits : List Bool → ℕ

Decode a big-endian binary list to a natural number.

Equations

• Nat.fromBits [] = 0
• Nat.fromBits (b :: rest) = (if b = true then 1 else 0) * 2 ^ rest.length + Nat.fromBits rest

theorem Nat.fromBits_lt_pow_length (l : List Bool) : fromBits l < 2 ^ l.length

Decoded values are bounded by 2 ^ length.

theorem Nat.fromBits_toBits_mod (w val : ℕ) : fromBits (w.toBits val) = val % 2 ^ w

fromBits ∘ toBits w reduces any input modulo 2 ^ w.

theorem Nat.fromBits_toBits {w val : ℕ} (hv : val < 2 ^ w) : fromBits (w.toBits val) = val

Nat.fromBits is a left inverse of Nat.toBits on values below 2 ^ w.

theorem Nat.toBits_add_pow_mul (w val c : ℕ) : w.toBits (val + c * 2 ^ w) = w.toBits val

Adding a multiple of 2^w does not change the low w encoded bits.

theorem Nat.toBits_fromBits (bits : List Bool) : bits.length.toBits (fromBits bits) = bits

Fixed-width encoding recovers every bit list from its decoded value.

theorem Nat.fromBits_inj_of_length_eq {first second : List Bool} (hlen : first.length = second.length) (hvalue : fromBits first = fromBits second) : first = second

Decoding is injective among bit lists of the same width.

def Nat.toBitsLE (width value : ℕ) : List Bool

Little-endian fixed-width bits, with the least significant bit first.

Equations

• width.toBitsLE value = (width.toBits value).reverse

def Nat.fromBitsLE (bits : List Bool) : ℕ

Decode a little-endian bit list.

Equations

• Nat.fromBitsLE bits = Nat.fromBits bits.reverse

@[simp]

theorem Nat.length_toBitsLE (width value : ℕ) : (width.toBitsLE value).length = width

Little-endian encoding has exactly the requested width.

theorem Nat.fromBitsLE_toBitsLE_mod (width value : ℕ) : fromBitsLE (width.toBitsLE value) = value % 2 ^ width

Little-endian decoding of a fixed-width encoding truncates modulo 2^width.

theorem Nat.fromBitsLE_toBitsLE {width value : ℕ} (hvalue : value < 2 ^ width) : fromBitsLE (width.toBitsLE value) = value

Little-endian encoding exactly round-trips values that fit the width.

theorem Nat.toBitsLE_fromBitsLE (bits : List Bool) : bits.length.toBitsLE (fromBitsLE bits) = bits

Every little-endian list is recovered at its own fixed width.

theorem Nat.fromBitsLE_lt_pow_length (bits : List Bool) : fromBitsLE bits < 2 ^ bits.length

A little-endian list decodes below 2 raised to its width.

theorem Nat.fromBitsLE_inj_of_length_eq {first second : List Bool} (hlen : first.length = second.length) (hvalue : fromBitsLE first = fromBitsLE second) : first = second

Little-endian decoding is injective at a fixed width.

theorem Nat.fromBitsLE_cons (bit : Bool) (bits : List Bool) : fromBitsLE (bit :: bits) = (if bit = true then 1 else 0) + 2 * fromBitsLE bits

Little-endian decoding exposes its least-significant head bit.

theorem Nat.fromBitsLE_bits (value : ℕ) : fromBitsLE value.bits = value

Decoding the canonical variable-width little-endian bits recovers the original natural number.

theorem Nat.toBitsLE_size (value : ℕ) : value.size.toBitsLE value = value.bits

The minimal fixed-width little-endian encoding is exactly the canonical variable-width bit list.

theorem Nat.size_le_log_two_add_one (value : ℕ) : value.size ≤ log 2 value + 1

Binary digit width is at most floor-log base two plus one.

theorem Nat.size_eq_log_two_add_one {value : ℕ} (hvalue : value ≠ 0) : value.size = log 2 value + 1

Every positive natural has binary digit width exactly floor-log base two plus one.