Canonical addition from order and BIT

A generate/propagate formula defines binary carry in the least-significant-bit-first convention. Comparing all sum bits defines ordinary addition on every canonical universe Fin n, n ≥ 2. The result is nonmodular: an out-of-range sum has no satisfying result in the universe.

This is the PLUS portion of the arithmetic-definability foundation. The Bit Sum Lemma is proved in Ordered.BitSum; native TIMES and full-tuple BIT are constructed in Ordered.Multiplication and Ordered.TupleBit. Numeric-preserving full-tuple composition is supplied in Ordered.FullTuple.Composition.

Main definitions

• Cslib.Logic.FO.Ordered.carryFormula: a carry generated below the given bit position.
• Cslib.Logic.FO.Ordered.addition: a single native formula for exact canonical addition.

Main results

• Cslib.Logic.FO.Ordered.realize_addition: the formula means natural-number addition.

References

• N. Immerman, Descriptive Complexity, Proposition 1.9 and the PLUS part of Theorem 1.17(1). Canonical BIT indexes from the least significant end, reversing the string orientation used in Proposition 1.9.
• Reuses Lean's BitVec.carry_succ and BitVec.getLsbD_add, and the library's source/link propagation characterization.

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

A lower bit generates a carry and every intervening bit propagates it. The two quantifiers range over positions in the canonical universe, with bit zero least significant.

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

Exact addition, expressed by comparing the result bits with input bits and generated carries. The formula is independent of the universe size and uses only native order, BIT and quantifiers.

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

The formula defines ordinary natural-number addition, including out-of-range rejection.

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

No element of the universe can represent an out-of-range sum.