The three sizes of the Bit Sum Lemma, and that they fit

DescriptiveComplexity.TimesBitDef – multiplication of ranks in the bit logic, the last step between the machine model and AC⁰ – rests on counting the ones of a P-bit word, P being the number of bit positions (DescriptiveComplexity.posCount). The count is done in three nested packings, and each of them has to fit in one element, that is, below the place value 2 ^ (P - 1), which is the only size a universe is guaranteed to have room for. This file fixes the three sizes and proves that they fit, with no formula and no structure in sight: it is the arithmetic that decides whether the packings of the Bit Sum Lemma exist at all.

The sizes

• Level 1 cuts the P positions into blocks of DescriptiveComplexity.BitSum.lvl1Block positions and keeps, in each block, the number of ones below it – a number ≤ P, so a field of DescriptiveComplexity.BitSum.lvl1Width bits (DescriptiveComplexity.BitSum.lt_two_pow_lvl1Width). The block is twice the field, so the packing occupies half the tape and its top bit stays below the top position.
• Level 2 does the same one size down, inside a single block: sub-blocks of DescriptiveComplexity.BitSum.lvl2Block positions, with a field of DescriptiveComplexity.BitSum.lvl2Width bits holding a number ≤ lvl1Block (DescriptiveComplexity.BitSum.lvl1Block_lt_two_pow_lvl2Width).
• Level 3 counts the ones of one sub-block by a table indexed by its value: lvl2Block + 1 sections of 2 ^ lvl2Block bits each. That the table fits is DescriptiveComplexity.BitSum.table_lt, and it is the inequality the whole design turns on.

Why two levels cannot do it

Level 1 needs its field to hold P, so 2 ^ lvl1Block > P; a table indexed by the value of a level-1 block would need (lvl1Block + 1) · 2 ^ lvl1Block < P. The two are contradictory, which is the arithmetic form of the packing obstruction: a level's items and its fields are paired by co-location, and a level whose fields are wider than the gap between its items cannot be co-located. Three levels are compatible because the table is indexed by a sub-block, whose value is quadratic in lvl1Width and so far below P.

The threshold

Everything holds once 2 ^ 20 ≤ P, which is DescriptiveComplexity.BitSum.le_posCount_of_card in terms of the universe: a universe with more than 2 ^ (2 ^ 20 - 1) elements. The bound is crude on purpose – it is discharged once and for all by DescriptiveComplexity.BitDef.of_large (LogTime/Small.lean), which turns a statement about the large universes into a statement about all of them, so nothing downstream carries it.

Two facts about Nat.size

theorem DescriptiveComplexity.BitSum.size_le_self (m : ℕ) : m.size ≤ m

The width of a number is at most the number.

theorem DescriptiveComplexity.BitSum.two_pow_size_pred_le {m : ℕ} (hm : 0 < m) : 2 ^ (m.size - 1) ≤ m

A number of k bits is at least 2 ^ (k - 1).

theorem DescriptiveComplexity.BitSum.two_pow_size_le {m : ℕ} (hm : 0 < m) : 2 ^ m.size ≤ 2 * m

…and less than twice itself.

The three sizes

def DescriptiveComplexity.BitSum.lvl1Width (P : ℕ) : ℕ

The width of a level-1 field: enough bits to hold a count of ones, which is at most the number of positions.

Equations

• DescriptiveComplexity.BitSum.lvl1Width P = P.size

def DescriptiveComplexity.BitSum.lvl1Block (P : ℕ) : ℕ

The length of a level-1 block: twice the field, so that the packing uses half the tape and stays below the top position.

Equations

• DescriptiveComplexity.BitSum.lvl1Block P = 2 * DescriptiveComplexity.BitSum.lvl1Width P

def DescriptiveComplexity.BitSum.lvl2Width (P : ℕ) : ℕ

The width of a level-2 field: enough bits to hold a count of ones within one level-1 block.

Equations

• DescriptiveComplexity.BitSum.lvl2Width P = (DescriptiveComplexity.BitSum.lvl1Block P).size

def DescriptiveComplexity.BitSum.lvl2Block (P : ℕ) : ℕ

The length of a level-2 sub-block: twice its field, for the same reason.

Equations

• DescriptiveComplexity.BitSum.lvl2Block P = 2 * DescriptiveComplexity.BitSum.lvl2Width P

theorem DescriptiveComplexity.BitSum.lt_two_pow_lvl1Width (P : ℕ) : P < 2 ^ lvl1Width P

A level-1 field holds a count of ones, there being at most P of them.

theorem DescriptiveComplexity.BitSum.lvl1Block_lt_two_pow_lvl2Width (P : ℕ) : lvl1Block P < 2 ^ lvl2Width P

A level-2 field holds a count of ones of one block.

That they fit

theorem DescriptiveComplexity.BitSum.cubic_step {t : ℕ} (ht : 21 ≤ t) : 240 * t ^ 2 + 240 * t + 79 ≤ 80 * t ^ 3

One doubling swallows the growth of a cube, from 21 on: the arithmetic core of the induction below.

theorem DescriptiveComplexity.BitSum.cube_lt_two_pow {s : ℕ} : 21 ≤ s → 80 * s ^ 3 + 1 < 2 ^ (s - 1)

The growth fact the three sizes rest on: a cube is eventually far below a power of two. 21 is where 80 s³ + 1 < 2 ^ (s - 1) starts to hold, and it is the only place a concrete number is chosen.

theorem DescriptiveComplexity.BitSum.lvl1Block_lt_two_pow_pred {P : ℕ} (hP : 2 ^ 20 ≤ P) : lvl1Block P < 2 ^ (P.size - 1)

Above the threshold, a level-1 block is a negligible part of the tape – the form in which the growth fact is used three times below.

theorem DescriptiveComplexity.BitSum.lvl1Block_lt {P : ℕ} (hP : 2 ^ 20 ≤ P) : lvl1Block P < P

A level-1 block fits on the tape, with room to spare.

theorem DescriptiveComplexity.BitSum.lvl2Block_lt_lvl1Block {P : ℕ} (hP : 2 ^ 20 ≤ P) : lvl2Block P < lvl1Block P

A level-2 sub-block is shorter than a level-1 block, so the second packing really does sit inside the first.

theorem DescriptiveComplexity.BitSum.table_lt {P : ℕ} (hP : 2 ^ 20 ≤ P) : (lvl2Block P + 1) * 2 ^ lvl2Block P < P - 1

The level-3 table fits in one element: lvl2Block + 1 sections of 2 ^ lvl2Block bits, all below the top position. This is the inequality that makes the three-level design exist, and the one that fails for two levels.

theorem DescriptiveComplexity.BitSum.two_le_lvl2Block {P : ℕ} (hP : 2 ^ 20 ≤ P) : 2 ≤ lvl2Block P

A sub-block is at least two positions long.

theorem DescriptiveComplexity.BitSum.size_le_two_pow_lvl2Block (P : ℕ) : P.size ≤ 2 ^ lvl2Block P

A sub-block's worth of values outnumbers the positions' own width: what the level-3 table's capacity condition needs on top of DescriptiveComplexity.BitSum.table_lt.

theorem DescriptiveComplexity.BitSum.two_le_lvl1Block {P : ℕ} (hP : 2 ^ 20 ≤ P) : 2 ≤ lvl1Block P

A block is at least two positions long.

theorem DescriptiveComplexity.BitSum.lvl1Block_succ_lt {P : ℕ} (hP : 2 ^ 20 ≤ P) : lvl1Block P + 1 < P

A block, and the position after it, leave room below the top.

theorem DescriptiveComplexity.BitSum.lt_two_pow_lvl1Block (P : ℕ) : P < 2 ^ lvl1Block P

A level-1 field holds a count of ones, in the form the running sum wants: the number of positions is below a block's worth of values.

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

…and so is a tail of two blocks, which is what level 1 hands to level 2.

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

There is room for a tail: three blocks and two sub-blocks fit below the top position with room to spare, which is what level 1's last chunk needs.

The threshold, on the universe

theorem DescriptiveComplexity.BitSum.le_posCount_of_card {A : Type} [LinearOrder A] [Finite A] (h : 2 ^ (2 ^ 20 - 1) < Nat.card A) : 2 ^ 20 ≤ posCount A

What the threshold asks of a universe: more than 2 ^ (2 ^ 20 - 1) elements. Every statement of the construction is proved for these and lifted to all universes by DescriptiveComplexity.BitDef.of_large, so the bound is never seen again.