Native conversion between scalar and word-valued radices

The input base is itself a fixed-length word, so it can represent the cardinality of the source universe. Input scalars are evaluated least-significant-first by exact Horner equations. They need not be smaller than that base; base one therefore also evaluates fixed scalar sums.

Main definitions

• Cslib.Logic.FO.Ordered.Radix.convert: evaluate scalar digits in a word-valued input base.

Main results

• Cslib.Logic.FO.Ordered.Radix.realize_convert: exact value semantics, including base one.

References

• N. Immerman, Descriptive Complexity, Exercise 1.33(3): the application to lexicographic tuple ranks.

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

Evaluate a fixed scalar sequence in a word-valued base, using exact Horner arithmetic.

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

When 1 < B, B ^ 3 fits in the universe and the word N is nonzero, convert L B N x z holds exactly when N and z are radix-B words and the digits x, read in base N, have the value of z.