Level 2: counting a middling word by its sub-blocks

The first instantiation of the running sum (DescriptiveComplexity.LogTime.BitSum.Sum): cut a word of m bits into sub-blocks, keep the running count in each, and let the table (DescriptiveComplexity.BitSum.PopShort) count one sub-block. The result has the same shape as the table's own statement –

DescriptiveComplexity.BitSum.PopMid m x y: y is the number of ones of the m-bit word x –

which is what lets level 1 be the very same construction one size up, with PopMid in the place PopShort occupies here.

Two things the certificate does not have to say

Which sub-block length to use. The length l is existentially quantified and constrained only to be a position index: soundness holds for any such l (DescriptiveComplexity.BitSum.popMid_sound takes no size hypothesis at all), and the completeness half is where a concrete l is chosen and the sizes of DescriptiveComplexity.LogTime.BitSum.Sizes are checked. This is what keeps the formula free of arithmetic it could not express: “the table fits” is a product of two variables, and no formula here ever has to state it.

Where the word ends. The certificate reads the running sum at any boundary past m, not at m itself, so the sub-block length never has to divide the word length. Counting further costs nothing, the word having no ones up there.

Counting past the end of a word

The level

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

y is the number of ones of the m-bit word x: a sub-block length, a boundary set, the running sums along it, and a boundary past m at which the running sum is read. The sub-block counts are supplied by the table.

Equations

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

theorem DescriptiveComplexity.BitSum.popMid_sound {A : Type} [LinearOrder A] [Finite A] {m x y : A} (hx : ∀ (i : ℕ), orank m ≤ i → (orank x).testBit i = false) (h : PopMid m x y) : orank y = onesBelow (orank x) (orank m)

The certificate is sound, with no condition on the sizes: whatever sub-block length is guessed, the running sum read past the end of the word is the number of its ones. The level below is used only through DescriptiveComplexity.BitSum.popShort_sound, which is itself unconditional above the index range.

Definability