The native TIMES formula

Multiplication is defined over canonical order and BIT by counting each binary multiplication column and checking its carries. Eight global words store the block-boundary carries, and sixteen local words store each block. Both ends of every block agree with the global words. The first and last carries are zero; exact PLUS and shifts prohibit modular overflow.

One fixed finite formula covers small inputs. The packed branch has witnesses for every universe of size at least 257, including sizes between powers of two. Neither branch uses multiplication in its syntax: only fixed literal scales, PLUS, exact shifts, and the proved native Bit Sum.

Main definitions

• Cslib.Logic.FO.Ordered.multiplication: one native multiplication formula.

Main results

• Cslib.Logic.FO.Ordered.realize_multiplication: exact natural-number product semantics.
• Cslib.Logic.FO.Ordered.not_realize_multiplication_of_le: rejection of every overflow candidate.

References

• N. Immerman, Descriptive Complexity, Theorem 1.17(1), using Lemma 1.18. The Bit Sum Lemma is historically due to Barrington, Immerman and Straubing [BIS90]. This packed carry-table construction is a proved variant of the source's alternating padded blocks and short running sums, not a transcription.

noncomputable def Cslib.Logic.FO.Ordered.multiplication (L : FirstOrder.Language) : (language L).Formula (Fin 3)

Native TIMES over canonical order and BIT, with ordinary, nonmodular product semantics.

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_multiplication {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : Fin 3 → Fin n) : (multiplication L).Realize v ↔ ↑(v 0) * ↑(v 1) = ↑(v 2)

The single native formula realizes exactly natural-number multiplication. In particular, no candidate output satisfies it when the product is outside Fin n.

theorem Cslib.Logic.FO.Ordered.not_realize_multiplication_of_le {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : Fin 3 → Fin n) (h : n ≤ ↑(v 0) * ↑(v 1)) : ¬(multiplication L).Realize v

No element represents a product outside the universe; truncation is not accepted.

theorem Cslib.Logic.FO.Ordered.existsUnique_multiplication {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (x y : Fin n) (hxy : ↑x * ↑y < n) : ∃! z : Fin n, (multiplication L).Realize ![x, y, z]

Every representable ordinary product has exactly one output.