Native arithmetic on fixed-length radix words

The radix is a source element, but a word may represent a value much larger than the source universe. Native PLUS and TIMES check only individual digit equations. Bounded digits and zero initial and final carries make these equations exact rather than modular.

Main definitions

• Cslib.Logic.FO.Ordered.mulEq: apply native TIMES to arbitrary terms.
• Cslib.Logic.FO.Ordered.Radix.digits: bound every digit by the radix.
• Cslib.Logic.FO.Ordered.Radix.cell, Cslib.Logic.FO.Ordered.Radix.affine: one affine digit equation, and multiplying one word by a digit and adding another word.

Main results

• Cslib.Logic.FO.Ordered.Radix.realize_affine: exact ordinary arithmetic, provided the radix is at least two and its cube fits in the source universe.

References

• N. Immerman, Descriptive Complexity, Exercise 1.33(3) and Theorem 1.17(1): the digit construction implements the suggested arithmetic with the native arithmetic of the theorem.

noncomputable def Cslib.Logic.FO.Ordered.mulEq (L : FirstOrder.Language) {α : Type u_1} (x y z : (language L).Term α) : (language L).Formula α

Apply native TIMES to three arbitrary terms.

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_mulEq {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (x y z : (language L).Term α) (v : α → Fin n) : (mulEq L x y z).Realize v ↔ ↑(FirstOrder.Language.Term.realize v x) * ↑(FirstOrder.Language.Term.realize v y) = ↑(FirstOrder.Language.Term.realize v z)

mulEq L x y z holds iff the product of x and y equals z.

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

Every word digit is strictly below the radix.

noncomputable def Cslib.Logic.FO.Ordered.Radix.cell (L : FirstOrder.Language) {α : Type u_1} (B a b y c z c' : (language L).Term α) : (language L).Formula α

One exact affine digit equation, with all its scalar intermediate values checked.

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

Multiply a word by a coefficient at most the radix and add another word, rejecting final overflow. Allowing the radix itself as coefficient also provides exact word shifts.

@[simp]

theorem Cslib.Logic.FO.Ordered.Radix.realize_digits {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} {d : ℕ} (B : (language L).Term α) (x : Fin d → (language L).Term α) (v : α → Fin n) : (digits L B x).Realize v ↔ ∀ (i : Fin d), ↑(FirstOrder.Language.Term.realize v (x i)) < ↑(FirstOrder.Language.Term.realize v B)

digits L B x holds iff every digit x i is strictly less than B.

theorem Cslib.Logic.FO.Ordered.Radix.realize_cell {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (B a b y c z c' : (language L).Term α) (v : α → Fin n) : (cell L B a b y c z c').Realize v ↔ ↑(FirstOrder.Language.Term.realize v a) * ↑(FirstOrder.Language.Term.realize v b) + ↑(FirstOrder.Language.Term.realize v y) + ↑(FirstOrder.Language.Term.realize v c) = ↑(FirstOrder.Language.Term.realize v z) + ↑(FirstOrder.Language.Term.realize v B) * ↑(FirstOrder.Language.Term.realize v c') ∧ ↑(FirstOrder.Language.Term.realize v a) * ↑(FirstOrder.Language.Term.realize v b) + ↑(FirstOrder.Language.Term.realize v y) + ↑(FirstOrder.Language.Term.realize v c) < n

cell L B a b y c z c' holds iff a * b + y + c = z + B * c' and a * b + y + c < n.

theorem Cslib.Logic.FO.Ordered.Radix.realize_affine {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} {d : ℕ} (B b : (language L).Term α) (x y 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) : (affine L B b x y z).Realize v ↔ ↑(FirstOrder.Language.Term.realize v b) ≤ ↑(FirstOrder.Language.Term.realize v B) ∧ (∀ (i : Fin d), ↑(FirstOrder.Language.Term.realize v (x i)) < ↑(FirstOrder.Language.Term.realize v B)) ∧ (∀ (i : Fin d), ↑(FirstOrder.Language.Term.realize v (y i)) < ↑(FirstOrder.Language.Term.realize v B)) ∧ (∀ (i : Fin d), ↑(FirstOrder.Language.Term.realize v (z i)) < ↑(FirstOrder.Language.Term.realize v B)) ∧ ↑(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 (x i))) + Nat.ofDigits (↑(FirstOrder.Language.Term.realize v B)) (List.ofFn fun (i : Fin d) => ↑(FirstOrder.Language.Term.realize v (y i))) = Nat.ofDigits (↑(FirstOrder.Language.Term.realize v B)) (List.ofFn fun (i : Fin d) => ↑(FirstOrder.Language.Term.realize v (z i)))

When the radix B is at least two and B ^ 3 fits in the universe, affine L B b x y z holds exactly when b ≤ B, the words x, y and z have digits below B, and their values satisfy b x + y = z.