Level 3: counting the ones of a short word, by a table indexed by its value

This is the base of the Bit Sum Lemma and the place where its circularity is broken. Levels 1 and 2 reduce “count the ones of a word” to “count the ones of a shorter word”, and that cannot go on for ever: at the bottom something has to count outright. Here it is, and the trick is that a lookup is a bit read at an index, so a table indexed by the value of a short word costs nothing that a product would cost:

Guess a table D cut into sections of 2 ^ ℓ bits, one per possible count. The bit of section c at offset v says “v has c ones”. Sections are the boundary set of LogTime/BitSum/Blocks.lean, so the walk over counts is a walk over boundaries, and the entry for v in section c is at the index boundary + v – an addition.

Why this pins the table, and pins it locally

The table is not defined, it is constrained, by three conditions that mention only neighboring sections (DescriptiveComplexity.BitSum.TableOk):

• section 0 is set exactly at v = 0 – no ones means no word;
• no later section is set at v = 0;
• section c + 1 is set at v exactly when section c is set at v with its lowest one cleared (DescriptiveComplexity.BitSum.ClearLow).

Every one of those is a recursion on the value, never on the count, so no condition ever has to say “and now do this c times”. Soundness (DescriptiveComplexity.BitSum.table_sound) is then an induction on the count, and it needs nothing about the layout beyond the table fitting – the discipline LogTime/Pow.lean established.

Two things the conditions do not say

They do not say where the table stops: sections above ℓ are all zero and satisfy the recursion, so the guess simply runs out of ones to describe. And the step is guarded by DescriptiveComplexity.IsLowIx, for the reason the counter's step is: above the top position an element has no bits, so a condition demanded there would be unsatisfiable rather than merely idle.

The table

def DescriptiveComplexity.BitSum.TableOk {A : Type} [LinearOrder A] [Finite A] (g B D : A) : Prop

The conditions on the table: the bit of the section of count c at offset v says “v has c ones”, pinned by a recursion on v alone.

Equations

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

theorem DescriptiveComplexity.BitSum.table_sound {A : Type} [LinearOrder A] [Finite A] {g B D l : A} (hgpos : 0 < orank g) (hB : IsBlockSet g B) (hT : TableOk g B D) (hbits : orank g = 2 ^ orank l) (j : ℕ) (b v i : A) : orank b = orank g * j → v < g → orank b + orank v = orank i → IsLowIx i → (BitIx i D ↔ onesBelow (orank v) (orank l) = j)

The table says what it is meant to say: the entry of the section of count j at offset v holds exactly when v has j ones. The induction is on the count; each step is one application of the recursion on the value.

theorem DescriptiveComplexity.BitSum.exists_tableOk {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {g B l : A} (hgpos : 0 < orank g) (hbits : orank g = 2 ^ orank l) (hB : IsBlockSet g B) (hfit : (orank l + 1) * orank g < posCount A - 1) : ∃ (D : A), TableOk g B D

The table exists: its bit at the index i says that the value i names has the count i names, which is a statement about i alone – so the guess is a bit vector, and it fits by DescriptiveComplexity.BitSum.table_lt.

Counting the ones of a short word

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

y is the number of ones of the l-bit word x: the level-3 certificate in one existential – the section width, the boundaries, the counter, the table, and the section whose counter is y, whose entry at x is set.

Equations

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

theorem DescriptiveComplexity.BitSum.popShort_sound {A : Type} [LinearOrder A] [Finite A] {l x y : A} (hl : orank l < posCount A) (h : PopShort l x y) : orank y = onesBelow (orank x) (orank l)

The certificate is sound: whatever is guessed, the section it points at is the one holding the count of x.

theorem DescriptiveComplexity.BitSum.popShort_of_eq {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {l x y : A} (hfit : (orank l + 1) * 2 ^ orank l < posCount A - 1) (hcap : posCount A ≤ 2 ^ orank l * 2 ^ 2 ^ orank l) (hxl : orank x < 2 ^ orank l) (hy : orank y = onesBelow (orank x) (orank l)) : PopShort l x y

The certificate exists, once the table fits and the counter's fields are wide enough: this is the completeness half of level 3, and every element it guesses has already been built.

Definability

theorem DescriptiveComplexity.BitSum.bitDef_tableOk {L : FirstOrder.Language} {α : Type} (g B D : α) : BitDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (v : α → x) => TableOk (v g) (v B) (v D)

The table's conditions are first-order in the bit logic.

theorem DescriptiveComplexity.BitSum.bitDef_popShort {L : FirstOrder.Language} {α : Type} (l 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) => PopShort (v l) (v x) (v y)

Level 3 is a formula: the whole certificate, guessed in one block.