Native multiplication of radix words

A fixed number of Horner rounds multiplies a long word by another fixed-length word. Each round first multiplies the original word by one digit, then shifts the accumulating product and adds that contribution. This handles leading zero multiplier digits without asking an unnecessarily large shift of the original word to fit.

Main definitions

• Cslib.Logic.FO.Ordered.Radix.multiply: exact multiplication of fixed-length words.

Main results

• Cslib.Logic.FO.Ordered.Radix.realize_multiply: ordinary word-product semantics, with overflow rejected by the affine checks.

References

• N. Immerman, Descriptive Complexity, Exercise 1.33(3): this is an explicit radix implementation of the tuple arithmetic suggested there.

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

Fixed-length Horner multiplication, using two exact affine checks per multiplier digit.

theorem Cslib.Logic.FO.Ordered.Radix.realize_multiply {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} {d m : ℕ} (B : (language L).Term α) (x : Fin d → (language L).Term α) (y : Fin m → (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) : (multiply L B x y z).Realize v ↔ (∀ (i : Fin d), ↑(FirstOrder.Language.Term.realize v (x i)) < ↑(FirstOrder.Language.Term.realize v B)) ∧ (∀ (i : Fin m), ↑(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)) ∧ 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 m) => ↑(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 1 < B and B ^ 3 fits in the universe, multiply L B x y z holds exactly when x, y and z are radix-B words and the value of z is the product of those of x and y.