Documentation

DescriptiveComplexity.LogTime.BitSum.Counter

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 ℕ #

source
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
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.BitSum.packVal_lt {g : ℕ} {f : ℕ → ℕ} {m : ℕ} :
    (∀ j < m, f j < 2 ^ g) → packVal g f m < 2 ^ (m * g)

    A packing fits below the block it stops at, provided every value fits in a field.

    Dependency graph
    source
    theorem DescriptiveComplexity.BitSum.packVal_window {g : ℕ} {f : ℕ → ℕ} {m j : ℕ} :
    (∀ j < m, f j < 2 ^ g) → j < m → packVal g f m / 2 ^ (j * g) % 2 ^ g = f j

    What a field of a packing holds: the j-th field is f j.

    Dependency graph
    source
    def DescriptiveComplexity.BitSum.counterVal (g m : ℕ) :
    ℕ

    The packed counters: the number whose j-th field holds j.

    Equations
    Instances For
      Dependency graph
      source
      theorem DescriptiveComplexity.BitSum.counterVal_lt {g m : ℕ} (h : m ≤ 2 ^ g) :
      counterVal g m < 2 ^ (m * g)

      The counters fit below the block they stop at, provided each index fits in a field – which is what m ≤ 2 ^ g says.

      Dependency graph
      source
      theorem DescriptiveComplexity.BitSum.counterVal_window {g m j : ℕ} (h : m ≤ 2 ^ g) (hj : j < m) :
      counterVal g m / 2 ^ (j * g) % 2 ^ g = j

      What a counter field holds: the j-th field of the packed counters is j.

      Dependency graph

      The counter of a boundary set #

      source
      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.
      Instances For
        Dependency graph
        source
        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.

        Dependency graph
        source
        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.

        Dependency graph

        Definability #

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

        The counter is first-order in the bit logic: two conditions, each a block of quantified indices over windows.

        Dependency graph