Exact binary coding of finite alphabets

An explicit enumeration gives a delimited, palindromic unary code for each letter. Encodings are injective, have linear length bounds, commute with word reversal, and are exactly the strings accepted by the partial decoder. Empty alphabets are supported, and only the empty word then has a valid encoding.

@[simp]

theorem Complexity.FiniteAlphabetCode.decode_encode {α : Type} (c : FiniteAlphabetCode α) (w : List α) : c.decode (c.encode w) = some w

Every encoded word is decoded exactly.

theorem Complexity.FiniteAlphabetCode.decode_eq_some_iff {α : Type} (c : FiniteAlphabetCode α) {bits : List Bool} {w : List α} : c.decode bits = some w ↔ c.encode w = bits

The decoder accepts precisely the chosen encodings.

theorem Complexity.FiniteAlphabetCode.encode_injective {α : Type} (c : FiniteAlphabetCode α) : Function.Injective c.encode

Encoding distinct words gives distinct binary strings.

theorem Complexity.FiniteAlphabetCode.length_le_encode {α : Type} (c : FiniteAlphabetCode α) (w : List α) : w.length ≤ (c.encode w).length

Encoded size is at least the source word length.

theorem Complexity.FiniteAlphabetCode.length_encode_le {α : Type} (c : FiniteAlphabetCode α) (w : List α) : (c.encode w).length ≤ (c.size + 1) * w.length

The alphabet enumeration determines a constant linear size bound.

theorem Complexity.FiniteAlphabetCode.encode_reverse_eq {α : Type} (c : FiniteAlphabetCode α) (w : List α) : c.encode w.reverse = (c.encode w).reverse

Palindromic symbol codes commute with reversal of the whole word.

theorem Complexity.FiniteAlphabetCode.decode_reverse_eq {α : Type} (c : FiniteAlphabetCode α) (bits : List Bool) : c.decode bits.reverse = Option.map List.reverse (c.decode bits)

Reversal preserves validity and reverses the decoded letters.

@[simp]

theorem Complexity.FiniteAlphabetCode.map_encode {α β : Type} (c : FiniteAlphabetCode α) (output : FiniteAlphabetCode β) (f : List α → List β) (w : List α) : c.map output f (c.encode w) = output.encode (f w)

A coded function has exactly its specified output on every encoded input.

theorem Complexity.FiniteAlphabetCode.map_invalid {α β : Type} (c : FiniteAlphabetCode α) (output : FiniteAlphabetCode β) (f : List α → List β) {bits : List Bool} (h : c.decode bits = none) : c.map output f bits = []

A coded function returns empty output on every invalid code.