The counter field: telling a block which block it is

Co-location (DescriptiveComplexity.LogTime.BitSum.Blocks) says where a block's field is, and that is enough to walk the blocks. It is not enough to name them: a step of the walk that has to know “this is block j” cannot compute j from the boundary j · g, that being a division. So the number is carried, in the field the same boundaries delimit, by a second guessed element:

DescriptiveComplexity.BitSum.IsCounter g B C: the window of C between two consecutive boundaries holds the index of the first – pinned by “the field at the least boundary is 0” and “consecutive fields differ by one”, and by nothing else.

This is the second half of the device, and LogTime/Pow.lean's ValAt is the same idea with a doubling gap. It is what level 3 of the Bit Sum Lemma (LogTime/BitSum/Table.lean) needs: its table's sections are indexed by a count of ones, and the section walk has to know which count it is at.

What the guard is for

The conditions are stated only where there is room: the step is required of a pair of boundaries whose second window ends below the top position (DescriptiveComplexity.IsLowIx). Without that guard the topmost field would have to be written above the top position, where an element has no bits, and no C would satisfy the conditions at all. With it, DescriptiveComplexity.BitSum.counter_eq reads the counter wherever the layout has room, which is everywhere a construction uses it, and DescriptiveComplexity.BitSum.exists_isCounter builds one.

The capacity condition is the expected one: a field of g bits must hold every index it names, so posCount A ≤ orank g * 2 ^ orank g. For the gaps of §2.3 that is true with room to spare.

The packed counters, in ℕ

def DescriptiveComplexity.BitSum.packVal (g : ℕ) (f : ℕ → ℕ) : ℕ → ℕ

The number whose j-th field holds f j: fields of width g, one per block, for the first m blocks. The counter is the case f = id, and the running sum of LogTime/BitSum/Sum.lean is the general one.

Equations

• DescriptiveComplexity.BitSum.packVal g f 0 = 0
• DescriptiveComplexity.BitSum.packVal g f m.succ = DescriptiveComplexity.BitSum.packVal g f m + f m * 2 ^ (m * g)

The counter of a boundary set

def DescriptiveComplexity.BitSum.IsCounter {A : Type} [LinearOrder A] [Finite A] (g B C : A) : Prop

The counter element of a boundary set: between consecutive boundaries, C holds the number of the first – 0 at the least boundary, one more at each step. The step is asked only where the second window has room (DescriptiveComplexity.IsLowIx), since above the top position an element has no bits to write in.

Equations

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

theorem DescriptiveComplexity.BitSum.counter_eq {A : Type} [LinearOrder A] [Finite A] {g B C : A} (hg : 0 < orank g) (hB : IsBlockSet g B) (hC : IsCounter g B C) (b b' c : A) : BitIx b B → orank b + orank g = orank b' → IsLowIx b' → WindowAt b b' C c → orank g * orank c = orank b

What the counter says: at a boundary, the field holds the number of the boundary. The induction is on that number, and it is the whole soundness half of the device.

theorem DescriptiveComplexity.BitSum.exists_isCounter {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {g B : A} (hg : 0 < orank g) (hB : IsBlockSet g B) (hcap : posCount A ≤ orank g * 2 ^ orank g) : ∃ (C : A), IsCounter g B C

A counter exists, once a field is wide enough to hold every index it names: the packed counters of DescriptiveComplexity.BitSum.counterVal, cut off where the tape runs out.

Definability