Counting ones, and the two atoms level 3 counts with

The Bit Sum Lemma is about how many ones a word has, and this file says what that means and gives the two bit-level operations its base level (LogTime/BitSum/Table.lean) breaks the circularity with.

The count

DescriptiveComplexity.BitSum.onesBelow x w is the number of ones of x among the first w positions. It is a Finset.card, not a recursion, because every statement about it is about changing one bit: clearing a set bit lowers the count by one (DescriptiveComplexity.BitSum.onesBelow_clear), and that single fact is the whole recursion the level-3 table is pinned by. The width is a parameter rather than “all of them” because levels 1 and 2 count ones below a position, not of a whole element.

The two atoms

• DescriptiveComplexity.BitSum.ClearLow x x' – x' is x with its lowest one cleared. It is first-order in ≤ and BIT (name the lowest set index, say every lower index is clear, and copy every bit but that one), the count drops by exactly one, and it exists whenever x ≠ 0. This is what lets the table for popcount be pinned locally, by a recursion on the value rather than on the count.
• DescriptiveComplexity.BitSum.IsPowIx i p – p is the place value 2 ^ i. In the index naming this is free (p is the element whose only bit is at i), which is the mirror image of DescriptiveComplexity.powArithDef, where the same statement in FO(≤, +, ×) cost a certificate. It is how a level gets the number of values a sub-block can take, which is the gap of the table's sections.

Counting ones, in ℕ

def DescriptiveComplexity.BitSum.onesBelow (x w : ℕ) : ℕ

The number of ones of x below the position w.

Equations

• DescriptiveComplexity.BitSum.onesBelow x w = {i ∈ Finset.range w | x.testBit i = true}.card

@[simp]

theorem DescriptiveComplexity.BitSum.onesBelow_zero (x : ℕ) : onesBelow x 0 = 0

theorem DescriptiveComplexity.BitSum.onesBelow_clear {x x' i w : ℕ} (hi : x.testBit i = true) (hiw : i < w) (hx' : ∀ (j : ℕ), x'.testBit j = (x.testBit j && decide (j ≠ i))) : onesBelow x' w + 1 = onesBelow x w

Clearing a one lowers the count by one – whichever one it is. The level-3 table clears the lowest, but the counting does not care.

Clearing the lowest one

def DescriptiveComplexity.BitSum.ClearLow {A : Type} [LinearOrder A] (x x' : A) : Prop

x' is x with its lowest one cleared: an index that is set with nothing set below it, and every other bit copied.

Equations

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

Place values, in the index naming

def DescriptiveComplexity.BitSum.IsPowIx {A : Type} [LinearOrder A] (i p : A) : Prop

p is the place value of the index i: its only bit is at i. What DescriptiveComplexity.powArithDef had to prove in FO(≤, +, ×) is, in the index naming, this one line.

Equations

• DescriptiveComplexity.BitSum.IsPowIx i p = ∀ (j : A), DescriptiveComplexity.BitIx j p ↔ j = i

Definability