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

theorem DescriptiveComplexity.BitSum.chain_room {P : ℕ} (hP : 2 ^ 20 ≤ P) : lvl1Block P * (4 * lvl1Block P + 2) + 2 < P

The carry chains fit on the tape: a chain has at most 4 · lvl1Block fields (a block, or the tail, which is at most two blocks and change) of lvl1Block bits each, and that is far below the top position.

theorem DescriptiveComplexity.BitSum.two_posCount_lt_card {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (hP : 2 ^ 20 ≤ posCount A) : 2 * posCount A < Nat.card A

Two positions' worth of sums fit in the universe: what lets the local additions of a carry chain always name their result.

theorem DescriptiveComplexity.BitSum.card_le_two_pow_posCount {A : Type} [LinearOrder A] [Finite A] : Nat.card A ≤ 2 ^ posCount A

The universe is not bigger than its positions can address.

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.

theorem DescriptiveComplexity.BitSum.colWord_iff {A : Type} [LinearOrder A] [Finite A] {x y j w : A} : ColWord x y j w ↔ orank w = colWordN (orank x) (orank y) (orank j)

What the column word is worth: exactly DescriptiveComplexity.BitSum.colWordN of the ranks.

theorem DescriptiveComplexity.BitSum.exists_colWord {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x y j : A) : ∃ (w : A), ColWord x y j w

The column word exists: it is a sub-mask of y, hence a rank.

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

theorem DescriptiveComplexity.BitSum.colCount_sound {A : Type} [LinearOrder A] [Finite A] {x y j n : A} (h : ColCount x y j n) : orank n = colCountN (orank x) (orank y) (posCount A) (orank j)

What the column count is worth – with no condition at all, the Bit Sum Lemma's soundness being unconditional.

theorem DescriptiveComplexity.BitSum.exists_colCount {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {x y j : A} (hP : 2 ^ 20 ≤ posCount A) : ∃ (n : A), ColCount x y j n

Every column can be counted, above the threshold of the Bit Sum Lemma.

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.

theorem DescriptiveComplexity.BitSum.stepEq_sound {A : Type} [LinearOrder A] {n r r' t V : A} (h : StepEq n r r' t V) : orank r + orank n = 2 * orank r' + ((orank V).testBit (orank t)).toNat

What a step says, read on the ranks.

theorem DescriptiveComplexity.BitSum.stepEq_intro {A : Type} [LinearOrder A] [Finite A] {n r r' t V : A} (hs : orank r + orank n < Nat.card A) (hd : orank r' + orank r' < Nat.card A) (h : orank r + orank n = 2 * orank r' + ((orank V).testBit (orank t)).toNat) : StepEq n r r' t V

A true step is a certificate step, as soon as the two intermediate sums are small enough to be ranks.

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.

theorem DescriptiveComplexity.BitSum.rangeSum_of_eq {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {x y a e V : A} {Gv m : ℕ} (hP : 2 ^ 20 ≤ posCount A) (hGpos : 0 < Gv) (hPG : posCount A < 2 ^ Gv) (hm : 0 < m) (hae : orank a + m = orank e) (hroom : Gv * m + 1 < posCount A) (hV : orank V = intervalSum (colCountN (orank x) (orank y) (posCount A)) (orank a) m) : RangeSum x y a e V

The certificate exists, for the true sum: with any gap wide enough to hold a column count in one field and short enough for the chain to fit on the tape, the remainders of DescriptiveComplexity.BitSum.carryChain are packed into one element and every condition holds by the corresponding chain equation.

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_sound {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {x y z : A} (hP : 2 ^ 20 ≤ posCount A) (h : TimesCert x y z) : orank x * orank y = orank z

The certificate is sound: above the threshold, whatever was guessed, the three parts assemble to the product of the ranks.

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_succ {L : FirstOrder.Language} {α : Type} (x y : α) : 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) + 1 = orank (v y)

The successor of a rank is first-order in the bit logic: one guessed element of rank one.

theorem DescriptiveComplexity.BitSum.bitDef_colWord {L : FirstOrder.Language} {α : Type} (x y j w : α) : 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) => ColWord (v x) (v y) (v j) (v w)

The column word is a formula: one universal index, one addition, three bit reads.

theorem DescriptiveComplexity.BitSum.bitDef_colCount {L : FirstOrder.Language} {α : Type} (x y j n : α) : 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) => ColCount (v x) (v y) (v j) (v n)

The column count is a formula: the column word, handed to the Bit Sum Lemma.

theorem DescriptiveComplexity.BitSum.bitDef_stepEq {L : FirstOrder.Language} {α : Type} (n r r' t V : α) : BitDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (v : α → x) => StepEq (v n) (v r) (v r') (v t) (v V)

A chain step is a formula: two additions, a successor, a bit read and an equality, under two guessed intermediate sums.

theorem DescriptiveComplexity.BitSum.bitDef_rangeSum {L : FirstOrder.Language} {α : Type} (x y a e V : α) : 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) => RangeSum (v x) (v y) (v a) (v e) (v V)

A range of columns is a formula: the boundary set, the counter, the packed chain, and the three conditions – each a block of quantified indices over windows, the counts entering through DescriptiveComplexity.BitSum.bitDef_colCount.

theorem DescriptiveComplexity.BitSum.bitDef_timesCert {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) => TimesCert (v x) (v y) (v z)

The whole certificate is a formula: eleven guessed elements and the conditions, every one of them built from the pieces above.

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.