TIMES from BSUM: multiplication of ranks, in the bit logic

The last step of Immerman 1999 Thm 1.17(1), and the one the textbook leaves entirely to the reader: with the Bit Sum Lemma in hand (DescriptiveComplexity.BitSum.PopAll), define orank x * orank y = orank z in FO(≤, BIT). The design gap it closes is recorded in the module docstring of DescriptiveComplexity.LogTime.BitSum.Columns; the certificate here has three layers, each guessed and pinned locally, none ever computing a product:

• A column (DescriptiveComplexity.BitSum.ColCount): the word whose ones are the pairs of set bits of x and y meeting at one column – a sub-mask of y, read off bit by bit – counted by the Bit Sum Lemma.
• A range of columns (DescriptiveComplexity.BitSum.RangeSum): the weighted sum Σ_t c_{a+t} 2 ^ t of the columns [a, e), certified by a carry chain: the remainders of the column-by-column addition, packed one field per column into a single element, walked with the boundary set and the counter of LogTime/BitSum/Blocks and Counter, each step one DescriptiveComplexity.BitSum.StepEq – an addition and a bit of the result.
• The product (DescriptiveComplexity.BitSum.TimesCert): cut the columns into blocks of g with 2 ^ g > P, so a block sum has 2 g bits and the fields of the even (resp. odd) blocks tile an element exactly; one guessed element per parity, their windows certified by RangeSum, a tail from the last boundary to the top of the tape, and two additions put the product together. A no-overflow clause makes the columns end below the top, which is what confines the whole sum to the tape.

Soundness holds for whatever is guessed (DescriptiveComplexity.BitSum.rangeSum_sound takes no size hypothesis), the sizes are paid once in the completeness half (DescriptiveComplexity.BitSum.timesCert_of_eq, above the threshold of LogTime/BitSum/Sizes), and DescriptiveComplexity.BitSum.bitDef_times discharges the threshold with DescriptiveComplexity.BitDef.of_large. The result, DescriptiveComplexity.timesBitDef, is consumed in LogTime/Translate.lean, where it closes AC⁰ = FO(≤, BIT) – the machine model is AC⁰.

Two more sizes

One column

def DescriptiveComplexity.BitSum.ColWord {A : Type} [LinearOrder A] (x y j w : A) : Prop

The word of one column: the bit of w at i says that y has a one at i and x a one at the index completing i to j. Stated bit by bit, with the complement named by an addition.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.BitSum.ColCount {A : Type} [LinearOrder A] [Finite A] (x y j n : A) : Prop

The count of one column: the column word, counted by the Bit Sum Lemma.

Equations

• DescriptiveComplexity.BitSum.ColCount x y j n = ∃ (w : A), DescriptiveComplexity.BitSum.ColWord x y j w ∧ DescriptiveComplexity.BitSum.PopAll w n

One step of a carry chain

def DescriptiveComplexity.BitSum.StepEq {A : Type} [LinearOrder A] (n r r' t V : A) : Prop

One step of the carry chain: the incoming remainder plus the column count equals twice the outgoing remainder plus the bit of V at t – stated with the sum and the double as guessed elements, so that it is two additions, a bit read and a successor.

Equations

• One or more equations did not get rendered due to their size.

A range of columns, by a guessed carry chain

def DescriptiveComplexity.BitSum.RangeSum {A : Type} [LinearOrder A] [Finite A] (x y a e V : A) : Prop

The sum of the columns [a, e), certified: a gap, its boundary set and counter, and one element R carrying the remainders of the column-by-column addition, one field per column. The base pins the first column against the lowest bit of V; the step, guarded by the room it needs, pins each next column against the next bit, the counter naming the column; and the top names the field of the last column and reads it as the bits of V above the range – with nothing beyond them.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.BitSum.rangeSum_sound {A : Type} [LinearOrder A] [Finite A] {x y a e V : A} (h : RangeSum x y a e V) : ∃ (m : ℕ), 0 < m ∧ orank a + m = orank e ∧ orank V = intervalSum (colCountN (orank x) (orank y) (posCount A)) (orank a) m

The certificate is sound, whatever was guessed: the chain equations, walked from the first column, force V to be the weighted sum of the columns of the range – with no size hypothesis at all.

The product

def DescriptiveComplexity.BitSum.TimesCert {A : Type} [LinearOrder A] [Finite A] (x y z : A) : Prop

The whole certificate for orank x * orank y = orank z: the columns of the schoolbook product, cut into blocks at a guessed gap; the block sums of the even blocks written in the tiling fields of one element, those of the odd blocks in another, each field certified by a carry chain; the columns from the last boundary to the top of the tape as one more range; and two additions putting the three parts together. The no-overflow clause keeps every column on the tape, which is what makes the three parts everything there is.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.BitSum.timesCert_of_eq {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {x y z : A} (hP : 2 ^ 20 ≤ posCount A) (hz : orank x * orank y = orank z) : TimesCert x y z

The certificate exists for the product: the gap of LogTime/BitSum/Sizes, the boundaries of the even/odd split at twice that gap, a last boundary two blocks and change below the top, the block sums packed by DescriptiveComplexity.BitSum.packVal, and the tail; every window is a field of a packing and every range is DescriptiveComplexity.BitSum.rangeSum_of_eq.

theorem DescriptiveComplexity.BitSum.timesCert_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {x y z : A} (hP : 2 ^ 20 ≤ posCount A) : TimesCert x y z ↔ orank x * orank y = orank z

The multiplication of ranks, characterized: above the threshold, the certificate holds exactly for the products.

Definability

theorem DescriptiveComplexity.BitSum.bitDef_times {L : FirstOrder.Language} {α : Type} (x y z : α) : BitDef fun (x_1 : Type) (x_2 : L.Structure x_1) (x_3 : LinearOrder x_1) (x_4 : Finite x_1) (x_5 : Nonempty x_1) (v : α → x_1) => orank (v x) * orank (v y) = orank (v z)

Multiplication of ranks is bit-definable – the missing half of Immerman 1999 Thm 1.17(1), assembled: the certificate is a formula, it characterizes the products above the threshold, and DescriptiveComplexity.BitDef.of_large absorbs the threshold, the relation being numeric. Stated first on three named variables, then relabeled to any layout.