Native radix decoding

A source element is decoded by exact scalar quotient equations, with its final quotient required to be zero. Every intermediate scalar is at most the original element, so decoding works even when the universe size is not a power of two.

Main definitions

• Cslib.Logic.FO.Ordered.Radix.decode: decode a source element into a fixed-length word.

Main results

• Cslib.Logic.FO.Ordered.Radix.realize_decode: exact bounded-digit semantics.
• Cslib.Logic.FO.Ordered.Radix.exists_word: every value below the word capacity has witnesses.

References

• N. Immerman, Descriptive Complexity, Exercise 1.33(3): the full-tuple application.

noncomputable def Cslib.Logic.FO.Ordered.Radix.quotientEq (L : FirstOrder.Language) {α : Type u_1} (B x q r : (language L).Term α) : (language L).Formula α

The exact quotient equation x = r + B*q; a remainder bound is supplied separately.

noncomputable def Cslib.Logic.FO.Ordered.Radix.decode (L : FirstOrder.Language) {α : Type u_1} {d : ℕ} (B x : (language L).Term α) (w : Fin d → (language L).Term α) : (language L).Formula α

Decode a scalar by exact quotient equations, including a zero final quotient.

theorem Cslib.Logic.FO.Ordered.Radix.realize_quotientEq {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (B x q r : (language L).Term α) (v : α → Fin n) : (quotientEq L B x q r).Realize v ↔ ↑(FirstOrder.Language.Term.realize v x) = ↑(FirstOrder.Language.Term.realize v r) + ↑(FirstOrder.Language.Term.realize v B) * ↑(FirstOrder.Language.Term.realize v q)

theorem Cslib.Logic.FO.Ordered.Radix.realize_decode {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} {d : ℕ} (B x : (language L).Term α) (w : Fin d → (language L).Term α) (v : α → Fin n) (hB : 1 ≤ ↑(FirstOrder.Language.Term.realize v B)) : (decode L B x w).Realize v ↔ (∀ (i : Fin d), ↑(FirstOrder.Language.Term.realize v (w i)) < ↑(FirstOrder.Language.Term.realize v B)) ∧ Nat.ofDigits (↑(FirstOrder.Language.Term.realize v B)) (List.ofFn fun (i : Fin d) => ↑(FirstOrder.Language.Term.realize v (w i))) = ↑(FirstOrder.Language.Term.realize v x)

When 1 ≤ B, decode L B x w holds exactly when w is a radix-B word with the value of x.

theorem Cslib.Logic.FO.Ordered.Radix.exists_word {n d : ℕ} (B : Fin n) {z : ℕ} (hz : z < ↑B ^ d) : ∃ (w : Fin d → Fin n), (∀ (i : Fin d), ↑(w i) < ↑B) ∧ Nat.ofDigits (↑B) (List.ofFn fun (i : Fin d) => ↑(w i)) = z

Digit witnesses fit in the source universe even when the represented word does not.