Native multiplication columns

The contributing rows of column j are encoded by the bits x[t] ∧ y[j-t]. This word is always at most x, so it fits in every canonical universe containing x, not only universes whose size is a power of two. Native Bit Sum counts the rows, and PLUS checks the exact carry equation without modular overflow.

Main definitions

• Cslib.Logic.FO.Ordered.Multiplication.columnWord: the bitwise column formula.
• Cslib.Logic.FO.Ordered.Multiplication.columnCount: the exact column count.
• Cslib.Logic.FO.Ordered.Multiplication.carryStep: one nonmodular carry equation.

Main results

• Cslib.Logic.FO.Ordered.Multiplication.realize_columnCount: exact column-count semantics.
• Cslib.Logic.FO.Ordered.Multiplication.realize_carryStep: exact bounded carry semantics.

References

• N. Immerman, Descriptive Complexity, Theorem 1.17(1) and Lemma 1.18. The Bit Sum Lemma is due to Barrington, Immerman and Straubing [BIS90]. The carry equation is a variant of the source's short sums.

noncomputable def Cslib.Logic.FO.Ordered.Multiplication.columnWord (L : FirstOrder.Language) {α : Type u_1} (x y j w : (language L).Term α) : (language L).Formula α

A word marking the input bits contributing to one multiplication column.

noncomputable def Cslib.Logic.FO.Ordered.Multiplication.columnCount (L : FirstOrder.Language) {α : Type u_1} (x y j a : (language L).Term α) : (language L).Formula α

Native Bit Sum counts the contributing rows of a column.

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

One exact carry equation. All addition and doubling witnesses must fit in the universe.

@[simp]

theorem Cslib.Logic.FO.Ordered.Multiplication.realize_columnWord {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (x y j w : (language L).Term α) (v : α → Fin n) : (columnWord L x y j w).Realize v ↔ ↑(FirstOrder.Language.Term.realize v w) = BitString.mulColumnWord ↑(FirstOrder.Language.Term.realize v x) ↑(FirstOrder.Language.Term.realize v y) ↑(FirstOrder.Language.Term.realize v j)

@[simp]

theorem Cslib.Logic.FO.Ordered.Multiplication.realize_columnCount {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (x y j a : (language L).Term α) (v : α → Fin n) : (columnCount L x y j a).Realize v ↔ ↑(FirstOrder.Language.Term.realize v a) = BitString.mulColumn ↑(FirstOrder.Language.Term.realize v x) ↑(FirstOrder.Language.Term.realize v y) ↑(FirstOrder.Language.Term.realize v j)

columnCount L x y j a holds exactly when a is the number of rows contributing to column j of the product of x and y (BitString.mulColumn).

theorem Cslib.Logic.FO.Ordered.Multiplication.realize_carryStep {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (x y z i c c' : (language L).Term α) (v : α → Fin n) : (carryStep L x y z i c c').Realize v ↔ ↑(FirstOrder.Language.Term.realize v c) + BitString.mulColumn ↑(FirstOrder.Language.Term.realize v x) ↑(FirstOrder.Language.Term.realize v y) ↑(FirstOrder.Language.Term.realize v i) = ((↑(FirstOrder.Language.Term.realize v z)).testBit ↑(FirstOrder.Language.Term.realize v i)).toNat + 2 * ↑(FirstOrder.Language.Term.realize v c') ∧ ↑(FirstOrder.Language.Term.realize v c) + BitString.mulColumn ↑(FirstOrder.Language.Term.realize v x) ↑(FirstOrder.Language.Term.realize v y) ↑(FirstOrder.Language.Term.realize v i) < n

carryStep L x y z i c c' holds exactly when the carry c into column i plus its column count is bit i of z plus twice the outgoing carry c', and that sum fits in the universe.