Co-location: the one device the Bit Sum Lemma is built out of

Every packing of the Bit Sum Lemma has to answer the same question – given the item, where is its field? – and the answer is never “compute the product of the item's number with the field width”, which is exactly what a logic without multiplication cannot do. It is always:

Guess the boundaries, and put each item's field at the item. A set of positions is one element; “the next boundary is g further on” is PLUS on indices, which the index naming makes free; and if the walk over items is the walk over boundaries, no index is ever computed from an item.

This file is that device, once, for the whole construction: the boundary set (DescriptiveComplexity.BitSum.IsBlockSet) and the reader that takes a field out of an element (DescriptiveComplexity.BitSum.WindowAt). LogTime/Pow.lean is the same pattern with a doubling gap, written before it was worth factoring out; here the gap is constant, and that makes “consecutive boundaries” a plain addition instead of a “nothing in between” quantifier.

The two notions

• DescriptiveComplexity.BitSum.WindowAt b e x m: m is the number written in the bits of x from the index b (included) to the index e (excluded). It is DescriptiveComplexity.FieldAt read in the index naming – a bit-level statement rather than a division with remainder – and its semantics is DescriptiveComplexity.BitSum.windowAt_iff. Every layout in the construction is stated with it, and no bit is touched again.
• DescriptiveComplexity.BitSum.IsBlockSet g B: the bits of B are exactly the multiples of g that are not the top position. Three local conditions pin it (DescriptiveComplexity.BitSum.bitIx_iff_of_isBlockSet), and the downward one – every non-zero boundary has a boundary g below it – is what rules out a set that starts somewhere other than 0.

What is not here, and why

There is no “consecutive boundaries” relation: with a constant gap, b and b' are consecutive exactly when orank b + orank g = orank b', and that is an atom. The counter field – a second element carrying, in the field the same boundaries delimit, the number of the boundary – is the other half of the device and comes with the level it is first needed at.

Windows, in ℕ

theorem DescriptiveComplexity.BitSum.testBit_window (x a w k : ℕ) : (x / 2 ^ a % 2 ^ w).testBit k = (decide (k < w) && x.testBit (a + k))

What a window reads: the bits of x / 2 ^ a % 2 ^ w are those of x from a up, and nothing from w on.

Windows of an element

def DescriptiveComplexity.BitSum.WindowAt {A : Type} [LinearOrder A] (b e x m : A) : Prop

The window of x between the indices b and e, read as the number m: the bits of m are those of x shifted down by b, and m has none at or above the width. Stated bit by bit, so that it is an atom-for-atom formula of the bit logic (DescriptiveComplexity.BitSum.bitDef_windowAt).

Equations

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

theorem DescriptiveComplexity.BitSum.windowAt_iff {A : Type} [LinearOrder A] [Finite A] {b e x m : A} {w : ℕ} (hw : orank b + w = orank e) : WindowAt b e x m ↔ orank m = orank x / 2 ^ orank b % 2 ^ w

What a window is worth: at a window of width w, the number read is the w bits of x above the index b.

theorem DescriptiveComplexity.BitSum.exists_windowAt {A : Type} [LinearOrder A] [Finite A] {b e x : A} {w : ℕ} (hw : orank b + w = orank e) : ∃ (m : A), WindowAt b e x m

A window is always there to be read: what it reads is at most x, hence a rank of the universe.

The boundaries of a packing

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

A set of boundaries at a constant gap g: the least position is one, every boundary is below the top position, a boundary g further on is one, and every boundary other than the least has one g below it. The last condition is what pins the set down – without it it could start anywhere.

Equations

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

theorem DescriptiveComplexity.BitSum.bitIx_iff_of_isBlockSet {A : Type} [LinearOrder A] [Finite A] {g B : A} (hg : 0 < orank g) (h : IsBlockSet g B) (b : A) : BitIx b B ↔ orank g ∣ orank b ∧ IsLowIx b

What the conditions pin: the boundaries are exactly the multiples of the gap below the top position.

theorem DescriptiveComplexity.BitSum.exists_isBlockSet {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {g : A} (hP : 1 < posCount A) : ∃ (B : A), IsBlockSet g B

A boundary set exists: the multiples of the gap below the top position are a bit vector supported below that position, hence a rank (DescriptiveComplexity.exists_orank_testBit').

Definability

theorem DescriptiveComplexity.BitSum.bitDef_windowAt {L : FirstOrder.Language} {α : Type} (b e x m : α) : 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) => WindowAt (v b) (v e) (v x) (v m)

A window is first-order in the bit logic: two quantified indices, an addition, a comparison and two bit reads.

theorem DescriptiveComplexity.BitSum.bitDef_isBlockSet {L : FirstOrder.Language} {α : Type} (g B : α) : BitDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (v : α → x) => IsBlockSet (v g) (v B)

A boundary set is first-order in the bit logic.