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_le (x w : ℕ) : onesBelow x w ≤ w

There are no more ones than positions.

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

Nothing is counted only when there is nothing: with all bits below w, the count is 0 exactly at 0. This is the base case of the table.

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.

theorem DescriptiveComplexity.BitSum.onesBelow_of_clearLow {A : Type} [LinearOrder A] [Finite A] {x x' : A} {w : ℕ} (h : ClearLow x x') (hx : ∀ (i : ℕ), w ≤ i → (orank x).testBit i = false) : onesBelow (orank x') w + 1 = onesBelow (orank x) w

What clearing costs: one one.

theorem DescriptiveComplexity.BitSum.orank_lt_of_clearLow {A : Type} [LinearOrder A] [Finite A] {x x' : A} (h : ClearLow x x') : orank x' < orank x

Clearing a one makes the number smaller – so a recursion on “clear the lowest one” terminates, which is what the level-3 table's induction rests on.

theorem DescriptiveComplexity.BitSum.exists_clearLow {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {x : A} (hx : orank x ≠ 0) : ∃ (x' : A), ClearLow x x'

The lowest one can always be cleared: the result is smaller, hence a rank.

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

theorem DescriptiveComplexity.BitSum.orank_of_isPowIx {A : Type} [LinearOrder A] [Finite A] {i p : A} (hi : orank i < posCount A) (h : IsPowIx i p) : orank p = 2 ^ orank i

What a place value is worth.

theorem DescriptiveComplexity.BitSum.exists_isPowIx {A : Type} [LinearOrder A] [Finite A] {i : A} (hi : orank i < posCount A) : ∃ (p : A), IsPowIx i p

Every position has its place value, the two being the two namings of the same thing.

Definability

theorem DescriptiveComplexity.BitSum.bitDef_clearLow {L : FirstOrder.Language} {α : Type} (x x' : α) : 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) => ClearLow (v x) (v x')

Clearing the lowest one is first-order in the bit logic.

theorem DescriptiveComplexity.BitSum.bitDef_isPowIx {L : FirstOrder.Language} {α : Type} (i p : α) : BitDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (v : α → x) => IsPowIx (v i) (v p)

Being a place value is first-order in the bit logic – one quantifier and two atoms, where the other naming needed a two-element certificate.