The running sum: counting a long word by counting its chunks

Levels 1 and 2 of the Bit Sum Lemma are the same construction at two sizes: cut a word into chunks, keep in each chunk the number of ones below it, and verify one step by counting the ones of a single chunk – which is what the level below is for. So it is written once here, with the chunk counter as a parameter:

DescriptiveComplexity.BitSum.SumOk c B x S Cnt: B delimits the chunks of length c, and the window of S in each chunk holds the number of ones of x below that chunk – pinned by “0 at the first chunk” and “one step adds the count of the chunk just passed”, the count being supplied by Cnt.

Level 2 instantiates Cnt with DescriptiveComplexity.BitSum.PopShort (the table), level 1 with level 2. Nothing else changes, and neither level ever has to know how the level below counts.

What the soundness needs of the level below

Two things only, and both are statements, not constructions: that Cnt is sound (its second argument is the number of ones of its first) and that it is total (every word has a count). DescriptiveComplexity.BitSum.sum_eq then gives the running sums their meaning by an induction on the chunk index, exactly as DescriptiveComplexity.BitSum.counter_eq does for the counter – of which this is the general form, a counter being the running sum of the constant word 1.

The arithmetic underneath

One identity carries the whole thing: DescriptiveComplexity.BitSum.onesBelow_add – the ones below k + c are those below k plus those of the chunk starting at k. The chunk is read with DescriptiveComplexity.BitSum.WindowAt, whose value is x / 2 ^ k % 2 ^ c, and the truncation is harmless because a window's own count ignores what was cut off (DescriptiveComplexity.BitSum.onesBelow_mod).

Splitting a count

theorem DescriptiveComplexity.BitSum.onesBelow_succ (x w : ℕ) : onesBelow x (w + 1) = onesBelow x w + if x.testBit w = true then 1 else 0

One more position, one more one to count if it is set.

theorem DescriptiveComplexity.BitSum.onesBelow_congr {x y w : ℕ} (h : ∀ i < w, x.testBit i = y.testBit i) : onesBelow x w = onesBelow y w

The count only looks at the bits it counts.

theorem DescriptiveComplexity.BitSum.onesBelow_add (x k c : ℕ) : onesBelow x (k + c) = onesBelow x k + onesBelow (x / 2 ^ k) c

Cutting a count in two: the ones below k + c are those below k, plus those of the chunk that starts at k. This is the whole of the running sum's step.

theorem DescriptiveComplexity.BitSum.onesBelow_mod (x c : ℕ) : onesBelow (x % 2 ^ c) c = onesBelow x c

A window's own count does not see what the window cut off.

The running sum of a chunked word

def DescriptiveComplexity.BitSum.SumOk {A : Type} [LinearOrder A] [Finite A] (c B x S : A) (Cnt : A → A → Prop) : Prop

The running sums of x along the chunks of length c: 0 at the first chunk, and one step adds the number of ones of the chunk just passed, as counted by Cnt. The step is guarded like the counter's, and for the same reason.

Equations

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

theorem DescriptiveComplexity.BitSum.sum_eq {A : Type} [LinearOrder A] [Finite A] {c B x S : A} {Cnt : A → A → Prop} (hc : 0 < orank c) (hB : IsBlockSet c B) (hS : SumOk c B x S Cnt) (hsound : ∀ (w n : A), orank w < 2 ^ orank c → Cnt w n → orank n = onesBelow (orank w) (orank c)) (j : ℕ) (b b' s : A) : orank b = orank c * j → BitIx b B → orank b + orank c = orank b' → IsLowIx b' → WindowAt b b' S s → orank s = onesBelow (orank x) (orank b)

What the running sum says: at the chunk starting at b, the window of S holds the number of ones of x below b. The level below is used only through its soundness and its totality.

theorem DescriptiveComplexity.BitSum.onesBelow_orank_le {A : Type} [LinearOrder A] [Finite A] (x : A) (k : ℕ) : onesBelow (orank x) k ≤ posCount A

A rank has no more ones than the universe has positions – so a running sum always fits in a field wide enough to hold posCount.

theorem DescriptiveComplexity.BitSum.exists_sumOk {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {c B x : A} {Cnt : A → A → Prop} (hc : 0 < orank c) (hB : IsBlockSet c B) (hsound : ∀ (w n : A), orank w < 2 ^ orank c → Cnt w n → orank n = onesBelow (orank w) (orank c)) (hcomp : ∀ (w : A), orank w < 2 ^ orank c → ∃ (n : A), Cnt w n) (hwide : ∀ (k : ℕ), onesBelow (orank x) k < 2 ^ orank c) : ∃ (S : A), SumOk c B x S Cnt

The running sums exist: the counts below the boundaries, packed into the fields those boundaries delimit. The one capacity condition is that a field hold a count of ones of the word being counted – weaker than the counter's, whose values run to the number of chunks – and the layout is DescriptiveComplexity.BitSum.packVal.

Definability

theorem DescriptiveComplexity.BitSum.bitDef_sumOk {L : FirstOrder.Language} {α : Type} {Cnt : (A : Type) → [LinearOrder A] → [Finite A] → A → A → A → Prop} (hCnt : ∀ {β : Type} (p w n : β), BitDef fun (A : Type) (x : L.Structure A) (x_1 : LinearOrder A) (x_2 : Finite A) (x_3 : Nonempty A) (v : β → A) => Cnt A (v p) (v w) (v n)) (p c B x S : α) : BitDef fun (A : Type) (x_1 : L.Structure A) (x_2 : LinearOrder A) (x_3 : Finite A) (x_4 : Nonempty A) (v : α → A) => SumOk (v c) (v B) (v x) (v S) (Cnt A (v p))

The running sum is first-order in the bit logic, given that the level below is: the parameter Cnt is a family of relations with one distinguished variable – the size the level below works at – which is what both instantiations need.