Canonical variable-width binary natural-number codes

This module packages Nat.bits as a canonical binary code for natural numbers. Bits are ordered least-significant first, and redundant high zeroes are rejected. In particular, zero has the unique empty code.

Unlike a prefix code, this representation relies on an enclosing framing layer to determine the field boundary. Complexitylib.Encoding.Pairing provides that framing for variable-length machine inputs.

def Complexity.BinaryNatCode.encode (value : ℕ) : List Bool

Encode a natural by its minimal little-endian binary expansion.

Equations

• Complexity.BinaryNatCode.encode value = value.bits

def Complexity.BinaryNatCode.decode? (bits : List Bool) : Option ℕ

Decode a natural only when the supplied bits are its minimal expansion.

This rejects every redundant high-zero representation, making encode and decode? an exact codec rather than merely a value interpretation.

Equations

• Complexity.BinaryNatCode.decode? bits = if (Nat.fromBitsLE bits).bits = bits then some (Nat.fromBitsLE bits) else none

@[simp]

theorem Complexity.BinaryNatCode.length_encode (value : ℕ) : (encode value).length = value.size

Canonical binary codes have exactly the standard binary digit width.

@[simp]

theorem Complexity.BinaryNatCode.decode?_encode (value : ℕ) : decode? (encode value) = some value

Decoding a canonical binary code recovers its value.

theorem Complexity.BinaryNatCode.decode?_eq_some_iff (bits : List Bool) (value : ℕ) : decode? bits = some value ↔ bits = encode value

Exact decoding succeeds precisely on the canonical code of the result.

theorem Complexity.BinaryNatCode.encode_injective : Function.Injective encode

The canonical binary natural-number encoding is injective.