Level 1: counting all the ones of an element

The top of the Bit Sum Lemma, and the same running sum once more, with level 2 in the place level 3 occupied at level 2: cut the whole tape into blocks of DescriptiveComplexity.BitSum.lvl1Block positions, keep the running count in each, and let DescriptiveComplexity.BitSum.PopMid count one block.

DescriptiveComplexity.BitSum.PopAll x y: y is the number of ones of x.

This is the Bit Sum Lemma, BSUM, and everything above it in the section is about using it rather than proving it.

The one thing this level has that the others do not: a tail

Levels 2 and 3 count a word that is short compared with the tape, so their walk can run past the end of the word and stop at a boundary with room to spare. Level 1 counts a word as long as the tape itself, and above the top position an element has no bits to pack a running sum into. So the last block is handled separately: the certificate reads the running sum at a boundary b, then counts the rest of x – the window from b to any index past the top – as one more chunk, with the same PopMid that verifies the steps, and adds the two.

That is why the statement takes no word-length parameter: the tail makes the count total by construction, and the answer is the number of ones of x, full stop.

The level

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

y is the number of ones of x – the Bit Sum Lemma's certificate: a block length, the boundaries, the running sums, a boundary b at which the sum is read, and the tail of x above b counted as one more chunk.

Equations

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

theorem DescriptiveComplexity.BitSum.popAll_sound {A : Type} [LinearOrder A] [Finite A] {x y : A} (h : PopAll x y) : orank y = onesBelow (orank x) (posCount A)

The certificate is sound: the running sum at b counts the ones below b, the tail counts the rest, and there is no rest above the top position. As at level 2, no size condition is needed – the block length is guessed, and soundness holds for whichever one is.

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

The certificate exists: the block length of DescriptiveComplexity.LogTime.BitSum.Sizes, the boundaries at that gap, the running sums, the last boundary that still has room for its field, and the tail of x above it counted as one more chunk by level 2.

Definability

theorem DescriptiveComplexity.BitSum.bitDef_popAll {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) => PopAll (v x) (v y)

The Bit Sum Lemma is a formula: level 2 enters it twice – once as the chunk counter of the running sum, once to count the tail.