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_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.

Definability