Binary numbers on enumerated positions

What an encoder of binary numbers needs, once and for all. An encoded universe lays its bit positions out as the image of an enumeration e : Fin N → A that is injective, hits exactly the positions, and reflects the order (DescriptiveComplexity.BinEnum). Then

• the rank of a position is its index (DescriptiveComplexity.BinEnum.bitRank_eq);
• the decoded number is the plain sum of place values (DescriptiveComplexity.BinEnum.binNum_eq_sum);
• a set of positions carrying the Nat.testBit digits of a number that fits decodes to that number (DescriptiveComplexity.BinEnum.binNum_eq_of_testBit).

The last statement is the one an encoding's faithfulness proof uses: the encoder writes w.testBit p at the position of index p, and the abstract semantics reads w back. Whatever else the universe holds – items, vertices, facts – plays no part.

structure DescriptiveComplexity.BinEnum {A : Type} {N : ℕ} (Le : A → A → Prop) (Posn : A → Prop) (e : Fin N → A) : Prop

The positions of a universe, enumerated in increasing order: the enumeration is injective, its range is the set of positions, and it reflects the order.

• injective : Function.Injective e

  Distinct indices are distinct positions.

• posn_iff (q : A) : Posn q ↔ ∃ (p : Fin N), q = e p

  The positions are exactly the enumerated elements.

• le_iff (p p' : Fin N) : Le (e p) (e p') ↔ p ≤ p'

  The order of the positions is the order of their indices.

theorem DescriptiveComplexity.BinEnum.bitRank_eq {A : Type} {N : ℕ} {Le : A → A → Prop} {Posn : A → Prop} {e : Fin N → A} (h : BinEnum Le Posn e) (p : Fin N) : bitRank Le Posn (e p) = ↑p

The rank of a position is its index.

theorem DescriptiveComplexity.BinEnum.binNum_eq_sum {A : Type} {N : ℕ} {Le : A → A → Prop} {Posn : A → Prop} {e : Fin N → A} (h : BinEnum Le Posn e) (b : A → Prop) : binNum Le Posn b = ∑ p : Fin N, if b (e p) then 2 ^ ↑p else 0

The decoded number is the sum of the place values of its bits.

theorem DescriptiveComplexity.BinEnum.binNum_eq_of_testBit {A : Type} {N : ℕ} {Le : A → A → Prop} {Posn : A → Prop} {e : Fin N → A} (h : BinEnum Le Posn e) (w : ℕ) (hw : w < 2 ^ N) (b : A → Prop) (hb : ∀ (p : Fin N), b (e p) ↔ w.testBit ↑p = true) : binNum Le Posn b = w

The decoding. A set of positions carrying the binary digits of a number that fits in N positions decodes to that number.

theorem DescriptiveComplexity.binNum_fin_of_testBit {N : ℕ} {Le : Fin N → Fin N → Prop} (hle : ∀ (a b : Fin N), Le a b ↔ a ≤ b) (w : ℕ) (hw : w < 2 ^ N) (b : Fin N → Prop) (hb : ∀ (p : Fin N), b p ↔ w.testBit ↑p = true) : binNum Le (fun (x : Fin N) => True) b = w

On the universe Fin N, ordered as usual and with every element a position, the Nat.testBit digits of a number below 2 ^ N decode to it.