Self-delimiting natural-number encoding

A terminated-unary prefix code for natural numbers. It extends Mathlib's unary encoding with one false terminator, allowing a decoder to recover one number and leave the remaining bits untouched.

def ComplexityTheory.NatPrefixCode.encode (value : ℕ) : BitString

Encode value as value true bits followed by one false terminator. The terminator makes the code self-delimiting inside a larger bitstring.

Equations

• ComplexityTheory.NatPrefixCode.encode value = Computability.unaryEncodeNat value ++ [false]

def ComplexityTheory.NatPrefixCode.decodePrefix? : BitString → Option (ℕ × BitString)

Decode one terminated-unary prefix and return the unused suffix. A bitstring containing only true bits is malformed because it has no terminator.

Equations

• ComplexityTheory.NatPrefixCode.decodePrefix? [] = none
• ComplexityTheory.NatPrefixCode.decodePrefix? (false :: suffix) = some (0, suffix)
• ComplexityTheory.NatPrefixCode.decodePrefix? (true :: bits) = do let __x ← ComplexityTheory.NatPrefixCode.decodePrefix? bits match __x with | (value, suffix) => some (value + 1, suffix)

def ComplexityTheory.NatPrefixCode.decode? (bits : BitString) : Option ℕ

Decode exactly one natural number. Unlike decodePrefix?, this rejects every nonempty trailing suffix.

Equations

• ComplexityTheory.NatPrefixCode.decode? bits = match ComplexityTheory.NatPrefixCode.decodePrefix? bits with | some (value, []) => some value | x => none

@[simp]

theorem ComplexityTheory.NatPrefixCode.length_encode (value : ℕ) : List.length (encode value) = value + 1

An encoded natural occupies exactly one bit per unary unit plus its terminator. This equation is the accounting rule used by larger encodings.

@[simp]

theorem ComplexityTheory.NatPrefixCode.decodePrefix?_encode_append (value : ℕ) (suffix : BitString) : decodePrefix? (encode value ++ suffix) = some (value, suffix)

Prefix decoding reverses encoding without consuming a caller-provided suffix. This is the compositional round-trip property needed by token decoders.

@[simp]

theorem ComplexityTheory.NatPrefixCode.decode?_encode (value : ℕ) : decode? (encode value) = some value

Exact decoding reverses canonical encoding. In plain language, every natural number survives an encode-decode round trip.

theorem ComplexityTheory.NatPrefixCode.decode?_encode_append_eq_none (value : ℕ) {suffix : BitString} (hsuffix : suffix ≠ []) : decode? (encode value ++ suffix) = none

A nonempty suffix makes an otherwise canonical code invalid for exact decoding. This prevents two adjacent objects from being mistaken for one.

@[simp]

theorem ComplexityTheory.NatPrefixCode.decodePrefix?_unaryEncodeNat (value : ℕ) : decodePrefix? (Computability.unaryEncodeNat value) = none

An unterminated run of true bits is rejected. The decoder therefore fails closed on truncated codes rather than inventing a value.

def ComplexityTheory.NatPrefixCode.encoding : BinaryEncoding ℕ

The terminated-unary functions form a Mathlib-compatible binary encoding.

Equations

• One or more equations did not get rendered due to their size.

theorem ComplexityTheory.NatPrefixCode.encode_injective : Function.Injective encode

Canonical terminated-unary encodings are unambiguous.