Documentation

DescriptiveComplexity.LogTime.BitSum.Sizes

The three sizes of the Bit Sum Lemma, and that they fit #

DescriptiveComplexity.TimesBitDef – multiplication of ranks in the bit logic, the last step between the machine model and AC⁰ – rests on counting the ones of a P-bit word, P being the number of bit positions (DescriptiveComplexity.posCount). The count is done in three nested packings, and each of them has to fit in one element, that is, below the place value 2 ^ (P - 1), which is the only size a universe is guaranteed to have room for. This file fixes the three sizes and proves that they fit, with no formula and no structure in sight: it is the arithmetic that decides whether the packings of the Bit Sum Lemma exist at all.

The sizes #

Why two levels cannot do it #

Level 1 needs its field to hold P, so 2 ^ lvl1Block > P; a table indexed by the value of a level-1 block would need (lvl1Block + 1) · 2 ^ lvl1Block < P. The two are contradictory, which is the arithmetic form of the packing obstruction: a level's items and its fields are paired by co-location, and a level whose fields are wider than the gap between its items cannot be co-located. Three levels are compatible because the table is indexed by a sub-block, whose value is quadratic in lvl1Width and so far below P.

The threshold #

Everything holds once 2 ^ 20 ≤ P, which is DescriptiveComplexity.BitSum.le_posCount_of_card in terms of the universe: a universe with more than 2 ^ (2 ^ 20 - 1) elements. The bound is crude on purpose – it is discharged once and for all by DescriptiveComplexity.BitDef.of_large (LogTime/Small.lean), which turns a statement about the large universes into a statement about all of them, so nothing downstream carries it.

Two facts about Nat.size #

The three sizes #

source
def DescriptiveComplexity.BitSum.lvl1Width (P : ℕ) :
ℕ

The width of a level-1 field: enough bits to hold a count of ones, which is at most the number of positions.

Equations
Instances For
    Dependency graph
    source
    def DescriptiveComplexity.BitSum.lvl1Block (P : ℕ) :
    ℕ

    The length of a level-1 block: twice the field, so that the packing uses half the tape and stays below the top position.

    Equations
    Instances For
      Dependency graph
      source
      def DescriptiveComplexity.BitSum.lvl2Width (P : ℕ) :
      ℕ

      The width of a level-2 field: enough bits to hold a count of ones within one level-1 block.

      Equations
      Instances For
        Dependency graph
        source
        def DescriptiveComplexity.BitSum.lvl2Block (P : ℕ) :
        ℕ

        The length of a level-2 sub-block: twice its field, for the same reason.

        Equations
        Instances For
          Dependency graph
          source
          theorem DescriptiveComplexity.BitSum.lt_two_pow_lvl1Width (P : ℕ) :
          P < 2 ^ lvl1Width P

          A level-1 field holds a count of ones, there being at most P of them.

          Dependency graph
          source
          theorem DescriptiveComplexity.BitSum.lvl1Block_lt_two_pow_lvl2Width (P : ℕ) :
          lvl1Block P < 2 ^ lvl2Width P

          A level-2 field holds a count of ones of one block.

          Dependency graph

          That they fit #

          source
          theorem DescriptiveComplexity.BitSum.table_lt {P : ℕ} (hP : 2 ^ 20 ≤ P) :
          (lvl2Block P + 1) * 2 ^ lvl2Block P < P - 1

          The level-3 table fits in one element: lvl2Block + 1 sections of 2 ^ lvl2Block bits, all below the top position. This is the inequality that makes the three-level design exist, and the one that fails for two levels.

          Dependency graph

          The threshold, on the universe #

          source
          theorem DescriptiveComplexity.BitSum.le_posCount_of_card {A : Type} [LinearOrder A] [Finite A] (h : 2 ^ (2 ^ 20 - 1) < Nat.card A) :
          2 ^ 20 ≤ posCount A

          What the threshold asks of a universe: more than 2 ^ (2 ^ 20 - 1) elements. Every statement of the construction is proved for these and lifted to all universes by DescriptiveComplexity.BitDef.of_large, so the bound is never seen again.

          Dependency graph