The bit layer of a finite ordered universe

An element of a finite linearly ordered universe is a number, its rank; this file gives access to that number one bit at a time, in the two ways a bit position can be named, and relates them.

Two namings, and what each is for

A bit position can be named by its index i, or by its place value, the element p whose rank is 2 ^ i. Both appear here, and neither is a variant of the other:

• DescriptiveComplexity.BitIx is the index naming – BIT(x, i), the primitive of the classical vocabulary FO(≤, BIT). It is total, needs no guard, and its bookkeeping is the arithmetic of the universe: the next position is i + 1, and “the bit k positions up” is an addition. It is what the logic and the machine model of DescriptiveComplexity.LogTime are built on, because reading a bit at a guessed index is the random access those machines have.
• DescriptiveComplexity.BitAt is the place-value naming, and it is what makes a bit first-order in FO(≤, +, ×) (DescriptiveComplexity.arithDef_bit): the bit of x at place value p is a division with remainder, x = u + v with 2p ∣ u and p ≤ v < 2p, all three of whose witnesses are below x, hence are ranks of the universe and are not lost to truncation. Being a place value is itself first-order – orank p ≠ 0 together with “every divisor is 1 or even” (DescriptiveComplexity.isPos_iff_forall_dvd).

DescriptiveComplexity.bitIx_iff_bitAt is the bridge, and it is one existential: BitIx i x is BitAt p x at the p of rank 2 ^ i. What that existential costs is the definability of the graph of i ↦ 2 ^ i (DescriptiveComplexity.PowArithDef) – Immerman 1999 Thm 1.17(2), and the single lemma on which the translation of the machine's logic into FO(≤, +, ×) rests. It is a named statement rather than an assumption, and it is proved: DescriptiveComplexity.powArithDef (LogTime/Pow.lean); see DescriptiveComplexity.LogTime.

The number of positions is Nat.clog 2 (Nat.card A) (DescriptiveComplexity.posCount), and the ranks are exactly the numbers whose bits live in that range; the top index is DescriptiveComplexity.IsTopIx, read off the bits of the greatest element and so needing no arithmetic on exponents.

What a bit vector can hold

A single element holds one bit per position, so it can carry a whole Bool-valued function of the positions – provided the value stays below the size of the universe. That is the reason for DescriptiveComplexity.exists_orank_testBit, stated with an explicit bit budget: below posCount A a bit vector is not in general a rank (the universe need not have a power of two elements), below posCount A - 1 it always is. That one-position gap is what forces the sweep simulation of DescriptiveComplexity.LogTime to carry the state of its last step separately, and it is the only place the arithmetic of the layer is not uniform.

Bits of a natural number

theorem DescriptiveComplexity.testBit_iff_two_pow_le_mod (x i : ℕ) : x.testBit i = true ↔ 2 ^ i ≤ x % 2 ^ (i + 1)

A bit is a comparison of the remainder: the bit of x at place value 2 ^ i is set exactly when x is at least 2 ^ i modulo 2 ^ (i + 1).

theorem DescriptiveComplexity.testBit_iff_exists_split (x i : ℕ) : x.testBit i = true ↔ ∃ (u : ℕ) (v : ℕ), u + v = x ∧ 2 ^ i ≤ v ∧ v < 2 ^ (i + 1) ∧ 2 ^ (i + 1) ∣ u

A bit is a splitting: the bit of x at place value 2 ^ i is set exactly when x splits as a multiple of 2 ^ (i + 1) plus a remainder between 2 ^ i and 2 ^ (i + 1). Every witness is at most x, which is what makes the statement survive the truncation of a finite universe.

theorem DescriptiveComplexity.testBit_iff_le_of_lt {x i : ℕ} (h : x < 2 ^ (i + 1)) : x.testBit i = true ↔ 2 ^ i ≤ x

Below 2 ^ (i + 1) a bit is just a comparison: the truncated case, where the doubling of the place value has overflowed the universe.

theorem DescriptiveComplexity.eq_two_pow_of_forall_dvd (p : ℕ) : p ≠ 0 → (∀ (d : ℕ), d ∣ p → d = 1 ∨ 2 ∣ d) → ∃ (i : ℕ), p = 2 ^ i

Powers of two, by their divisors: a nonzero number all of whose divisors are 1 or even is a power of two. This is the first-order reading of “p is a position”, and it needs no primality.

theorem DescriptiveComplexity.forall_dvd_of_eq_two_pow {p i : ℕ} (hp : p = 2 ^ i) (d : ℕ) : d ∣ p → d = 1 ∨ 2 ∣ d

The converse: every divisor of a power of two is 1 or even.

noncomputable def DescriptiveComplexity.bitsVal (b : ℕ → Bool) (m : ℕ) : ℕ

The value of a finite bit vector, as a sum of place values.

Equations

• DescriptiveComplexity.bitsVal b m = ∑ i ∈ Finset.range m, if b i = true then 2 ^ i else 0

theorem DescriptiveComplexity.bitsVal_succ (b : ℕ → Bool) (m : ℕ) : bitsVal b (m + 1) = bitsVal b m + if b m = true then 2 ^ m else 0

Peeling the top bit of a finite bit vector.

theorem DescriptiveComplexity.bitsVal_lt (b : ℕ → Bool) (m : ℕ) : bitsVal b m < 2 ^ m

theorem DescriptiveComplexity.testBit_bitsVal (b : ℕ → Bool) (m : ℕ) {i : ℕ} (hi : i < m) : (bitsVal b m).testBit i = b i

Positions of a finite ordered universe

noncomputable def DescriptiveComplexity.posCount (A : Type) [LinearOrder A] [Finite A] : ℕ

The number of bit positions of the ranks of A: the ranks are the numbers below Nat.card A, so they are exactly the numbers whose bits live below Nat.clog 2 (Nat.card A).

Equations

• DescriptiveComplexity.posCount A = Nat.clog 2 (Nat.card A)

theorem DescriptiveComplexity.two_pow_lt_card_iff_lt_posCount {A : Type} [LinearOrder A] [Finite A] (i : ℕ) : 2 ^ i < Nat.card A ↔ i < posCount A

A place value is that of a position exactly when it is a rank.

theorem DescriptiveComplexity.testBit_orank_eq_false {A : Type} [LinearOrder A] [Finite A] {x : A} {i : ℕ} (hi : posCount A ≤ i) : (orank x).testBit i = false

Above the positions, every rank has a zero bit.

def DescriptiveComplexity.IsPos {A : Type} [LinearOrder A] (p : A) : Prop

p is a position: its rank is a place value 2 ^ i. The element is the place value; the exponent never appears in a formula.

Equations

• DescriptiveComplexity.IsPos p = ∃ (i : ℕ), DescriptiveComplexity.orank p = 2 ^ i

noncomputable def DescriptiveComplexity.posExp {A : Type} [LinearOrder A] (p : A) : ℕ

The exponent of a position.

Equations

• DescriptiveComplexity.posExp p = Nat.log 2 (DescriptiveComplexity.orank p)

theorem DescriptiveComplexity.posExp_eq {A : Type} [LinearOrder A] {p : A} {i : ℕ} (h : orank p = 2 ^ i) : posExp p = i

theorem DescriptiveComplexity.orank_eq_two_pow_posExp {A : Type} [LinearOrder A] {p : A} (h : IsPos p) : orank p = 2 ^ posExp p

theorem DescriptiveComplexity.exists_isPos {A : Type} [LinearOrder A] [Finite A] {i : ℕ} (hi : i < posCount A) : ∃ (p : A), orank p = 2 ^ i

Every exponent in range is the exponent of a position.

theorem DescriptiveComplexity.isPos_iff_forall_dvd {A : Type} [LinearOrder A] [Finite A] (p : A) : IsPos p ↔ orank p ≠ 0 ∧ ∀ (d : A), (∃ (w : A), orank w * orank d = orank p) → orank d = 1 ∨ ∃ (e : A), orank e + orank e = orank d

Being a position is first-order: a nonzero rank all of whose divisors are 1 or even, with every divisor and cofactor a rank of the universe – which they are, being at most orank p.

theorem DescriptiveComplexity.exists_orank_testBit {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (b : ℕ → Bool) : ∃ (t : A), ∀ (i : ℕ), i + 1 < posCount A → (orank t).testBit i = b i

The bit budget of a trace: a bit vector supported below the top position is a rank, whatever the size of the universe.

theorem DescriptiveComplexity.exists_orank_testBit' {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (b : ℕ → Bool) : ∃ (t : A), (∀ (i : ℕ), i + 1 < posCount A → (orank t).testBit i = b i) ∧ ∀ (i : ℕ), posCount A ≤ i + 1 → (orank t).testBit i = false

The same, with the top positions pinned to zero: the element a bit vector names carries no bit at the top position, which is what a construction needs when it also has to say that nothing outside its layout is set.

The bit of an element at a position

def DescriptiveComplexity.BitAt {A : Type} [LinearOrder A] (p x : A) : Prop

The bit of x at the place value p, first-order in ≤, + and ×: either the doubling q = p + p exists, and then x splits as a multiple u of q plus a remainder v with p ≤ v < q; or it does not, and then x is below 2 p already and the bit is the comparison p ≤ x.

Equations

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

theorem DescriptiveComplexity.bitAt_iff {A : Type} [LinearOrder A] [Finite A] {p x : A} {i : ℕ} (hp : orank p = 2 ^ i) : BitAt p x ↔ (orank x).testBit i = true

BitAt is BIT: at a position of place value 2 ^ i, it is the i-th bit of the rank.

The bit of an element at an index

def DescriptiveComplexity.BitIx {A : Type} [LinearOrder A] (i x : A) : Prop

The bit of x at the index i: the BIT of the classical vocabulary FO(≤, BIT), the position being named by the element whose rank is the exponent. Total, and with no guard – above the bit positions of the universe every bit is simply clear.

Equations

• DescriptiveComplexity.BitIx i x = ((DescriptiveComplexity.orank x).testBit (DescriptiveComplexity.orank i) = true)

theorem DescriptiveComplexity.bitIx_iff {A : Type} [LinearOrder A] {i x : A} : BitIx i x ↔ (orank x).testBit (orank i) = true

theorem DescriptiveComplexity.orank_lt_posCount_of_bitIx {A : Type} [LinearOrder A] [Finite A] {i x : A} (h : BitIx i x) : orank i < posCount A

A bit that is set is at a position of the universe.

theorem DescriptiveComplexity.exists_isMax (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : ∃ (m : A), ∀ (k : A), k ≤ m

A finite nonempty order has a greatest element – the one a formula reads the top index off.

theorem DescriptiveComplexity.bitIx_iff_bitAt {A : Type} [LinearOrder A] [Finite A] {i x : A} : BitIx i x ↔ ∃ (p : A), orank p = 2 ^ orank i ∧ BitAt p x

The two namings agree: the bit at the index i is the bit at the place value 2 ^ i. The existential is the whole of the difference between the two readings of BIT, and DescriptiveComplexity.PowArithDef is what it costs.

def DescriptiveComplexity.IsTopIx {A : Type} [LinearOrder A] [Finite A] (i : A) : Prop

i is the top index: the highest bit position of the universe.

Equations

• DescriptiveComplexity.IsTopIx i = (DescriptiveComplexity.orank i + 1 = DescriptiveComplexity.posCount A)

def DescriptiveComplexity.IsLowIx {A : Type} [LinearOrder A] [Finite A] (i : A) : Prop

i is a low index: a bit position with a further one above it. What separates the two is the budget of DescriptiveComplexity.exists_orank_testBit: a guessed trace carries a bit at every low index, and the top one has to be carried apart.

Equations

• DescriptiveComplexity.IsLowIx i = (DescriptiveComplexity.orank i + 1 < DescriptiveComplexity.posCount A)

theorem DescriptiveComplexity.bitIx_max_of_isTopIx {A : Type} [LinearOrder A] [Finite A] {i m : A} (hm : ∀ (k : A), k ≤ m) (h : IsTopIx i) : BitIx i m

The greatest element has its highest bit at the top index: orank of it is Nat.card A - 1, which lies between 2 ^ (posCount A - 1) and 2 ^ posCount A. This is what lets a formula find the end of the tape without any arithmetic on exponents – it reads it off the bits of an element it already has.

theorem DescriptiveComplexity.lt_card_of_lt_posCount {A : Type} [LinearOrder A] [Finite A] {d : ℕ} (h : d < posCount A) : d < Nat.card A

Every index below the count is the rank of an element.

theorem DescriptiveComplexity.posCount_lt_card {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : posCount A < Nat.card A

The count of positions is itself a rank: there are never more bit positions than elements, so a formula may quantify over an index one above the top – which is what pins the absence of a carry out of the last position.

theorem DescriptiveComplexity.isTopIx_iff_bits {A : Type} [LinearOrder A] [Finite A] {i m : A} (hm : ∀ (k : A), k ≤ m) : IsTopIx i ↔ BitIx i m ∧ ∀ (k : A), i < k → ¬BitIx k m

The top index, read from the bits of the greatest element: it is the highest index carrying a bit there.

theorem DescriptiveComplexity.isLowIx_iff_bits {A : Type} [LinearOrder A] [Finite A] {i m : A} (hm : ∀ (k : A), k ≤ m) : IsLowIx i ↔ ∃ (k : A), i < k ∧ BitIx k m

A low index, read from the same bits: one with a bit of the greatest element strictly above it.

Definability of the bit layer

theorem DescriptiveComplexity.arithDef_lt {L : FirstOrder.Language} {α : Type} (x y : α) : ArithDef 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) => v x < v y

The strict order between two variables is definable.

theorem DescriptiveComplexity.arithDef_isZero {L : FirstOrder.Language} {α : Type} (x : α) : ArithDef 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) => orank (v x) = 0

A rank being zero is definable: x + x = x holds of the least element only.

theorem DescriptiveComplexity.arithDef_isOne {L : FirstOrder.Language} {α : Type} (x : α) : ArithDef 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) => orank (v x) = 1

A rank being one is definable: an idempotent nonzero rank.

theorem DescriptiveComplexity.arithDef_isPos {L : FirstOrder.Language} {α : Type} (x : α) : ArithDef 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) => IsPos (v x)

Being a position is definable, by DescriptiveComplexity.isPos_iff_forall_dvd.

theorem DescriptiveComplexity.arithDef_bit {L : FirstOrder.Language} {α : Type} (p x : α) : ArithDef 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) => BitAt (v p) (v x)

The bit relation is definable: DescriptiveComplexity.BitAt is a formula of FO(≤, +, ×), so the bit layer costs the logic nothing.

The naming bridge

The one thing the place-value naming does not hand over. Everything above is a formula of FO(≤, +, ×) outright; the index naming needs, on top of it, the graph of i ↦ 2 ^ i, and that is a theorem rather than a construction – the half of Immerman 1999 Thm 1.17 that goes from +, × to BIT at an exponent. It is named here, where its consumers are, and proved in DescriptiveComplexity.LogTime.Pow, which is where the certificate it is proved by can be stated.

def DescriptiveComplexity.PowArithDef (L : FirstOrder.Language) : Prop

The naming bridge: the graph of i ↦ 2 ^ i is a formula of FO(≤, +, ×), uniformly in the variable layout.

This is Immerman 1999 Thm 1.17(2), and it is proved: DescriptiveComplexity.powArithDef, by the packing argument that guesses the doubling chain of i. It is a def rather than a plain statement because every consumer needs it at its own variable layout; DescriptiveComplexity.BitDefinable is a logic over the index naming, and this is what turns its bit atom back into the place-value one.

Equations

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

theorem DescriptiveComplexity.PowArithDef.arithDef_bitIx {L : FirstOrder.Language} {α : Type} (h : PowArithDef L) (i x : α) : ArithDef 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) => BitIx (v i) (v x)

The bit at an index is first-order, given the bridge: guess the place value, and read the place-value bit there.