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

theorem DescriptiveComplexity.BitSum.onesBelow_eq_of_ge {x w k : ℕ} (hx : ∀ (i : ℕ), w ≤ i → x.testBit i = false) (hk : w ≤ k) : onesBelow x k = onesBelow x w

Counting further than the word is long changes nothing.

theorem DescriptiveComplexity.BitSum.onesBelow_le_of_bits {x w k : ℕ} (hx : ∀ (i : ℕ), w ≤ i → x.testBit i = false) : onesBelow x k ≤ w

A word has no more ones than it is long.

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.

theorem DescriptiveComplexity.BitSum.exists_popMid {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {m x : A} (hP : 2 ^ 20 ≤ posCount A) (hm : orank m < 2 ^ lvl2Block (posCount A)) (hroom : orank m + 2 * lvl2Block (posCount A) + 2 < posCount A) (hx : ∀ (i : ℕ), orank m ≤ i → (orank x).testBit i = false) : ∃ (y : A), PopMid m x y

The certificate exists: the sub-block length of DescriptiveComplexity.LogTime.BitSum.Sizes, the boundaries at that gap, the running sums along them, and the first boundary past the end of the word. All three size conditions of the table are discharged here, and nowhere else.

Definability

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

Level 2 is a formula, the level below entering it only through DescriptiveComplexity.BitSum.bitDef_popShort, passed to DescriptiveComplexity.BitSum.bitDef_sumOk as the chunk counter.