The doubling chain: i ↦ 2 ^ i is first-order in ≤, + and ×

DescriptiveComplexity.powArithDef – the graph of i ↦ 2 ^ i as a formula of FO(≤, +, ×), Immerman 1999 Thm 1.17(2) – is the lemma the AC⁰ reading of the machine model rested on, and this file proves it, by exhibiting a certificate that a first-order formula can check.

The certificate

The chain is the halving chain of the exponent: a, a / 2, a / 4, …, 0, of length ⌈log a⌉ ≤ log log n. Its place values 2 ^ (a / 2 ^ t) are positions, so the chain is a set of positions, that is, one guessed element Y – carrying the chain below its top, the top being the given p (DescriptiveComplexity.chainBelow). Consecutive positions q < q' of the chain are tied by

q' = q * q (the exponent doubles) or q' = 2 * (q * q) (it doubles and gains one),

which is a product of elements – available – rather than an addition of exponents, which is not. That is the whole reason the chain is guessed at all.

Why the exponents have to be carried, and where

The chain conditions alone leave the value of the top exponent free: they force index q' = 2 * index q + ε with ε read off which case fired, so they pin the top index only relative to the bottom. What ties it to the given i is a second guessed element E carrying, in the field between q and the next chain position (DescriptiveComplexity.FieldAt), the number index q. No pairing between the chain and the positions is then needed – the value sits at the place it describes – and the recursion becomes a relation between values, val q' = 2 * val q + ε, which is DescriptiveComplexity.val_eq_of_chain.

So the certificate is two elements, not three: the chain delimits its own fields, and no marks have to be guessed. That the value fits in the field it is given is DescriptiveComplexity.half_add_size_le, and it is exactly the right statement – the field between the positions of index k / 2 and k is k - k / 2 bits wide, and the value it must hold is k / 2.

Four consequences worth keeping:

• Soundness needs no condition on the layout. The formula never says where a field ends or that fields do not overlap: whatever the guess, each q reads some value, and the chain conditions force those values to be the indices. A garbage layout simply fails the conditions.
• The top field must not be written. Its value is a itself, needing log log n bits above position a, and there need be no room: 2 ^ a < n says nothing about 2 ^ (a + log log n). The value at the top is the given element i, so the fields carry only the rest of the chain, whose largest entry is a / 2 and which therefore fits below position a. The top position is also the one with no next chain position, so it is exactly the one with no field to read: the two facts are the same fact.
• The top position is left out of Y for a second reason. A set of positions is an element only if its value is a rank, and the chain including its top can exceed 2 ^ a, hence the universe – there is no room for a bit at p itself when n is barely above 2 ^ a. Leaving it out costs nothing, p being given, and the rest fits with room to spare: DescriptiveComplexity.chainBelow_lt.
• The chain conditions are between consecutive positions only. That is what DescriptiveComplexity.chainSet_le_half_of_lt buys – the predecessor of the entry k is k / 2 and nothing lies between – so a formula quantifying “q and q' in Y with nothing of Y between” sees exactly the pairs the recursion talks about.

What is here, in three layers

• The arithmetic, in ℕ: the chain as a set (DescriptiveComplexity.ChainSet), the fact that the predecessor of k in it is k / 2 (DescriptiveComplexity.chainSet_le_half_of_lt), the induction that turns the chain conditions into val k = k (DescriptiveComplexity.val_eq_of_chain), and the two elements a certificate guesses – DescriptiveComplexity.chainBelow, read back by DescriptiveComplexity.testBit_chainBelow, and DescriptiveComplexity.chainVals, read back by DescriptiveComplexity.chainVals_field. Both are ranks because both are below 2 ^ a (DescriptiveComplexity.chainBelow_lt, DescriptiveComplexity.chainVals_lt), the second by the capacity lemma DescriptiveComplexity.half_add_size_le.
• The certificate, as a property of four elements (DescriptiveComplexity.PowCert, over DescriptiveComplexity.InChain/ConsChain/ValAt), with both halves: DescriptiveComplexity.powCert_sound and DescriptiveComplexity.powCert_complete, conjoined in DescriptiveComplexity.powCert_iff.
• The formula, built with the DescriptiveComplexity.ArithDef API and the field reader DescriptiveComplexity.arithDef_fieldAt, giving DescriptiveComplexity.powArithDef.

The halving chain

def DescriptiveComplexity.ChainSet (a k : ℕ) : Prop

The halving chain of a: the exponents a / 2 ^ t, which are the indices of the positions a 2 ^ a certificate guesses.

Equations

• DescriptiveComplexity.ChainSet a k = ∃ (t : ℕ), k = a / 2 ^ t

theorem DescriptiveComplexity.chainSet_self (a : ℕ) : ChainSet a a

theorem DescriptiveComplexity.chainSet_zero (a : ℕ) : ChainSet a 0

theorem DescriptiveComplexity.chainSet_half {a k : ℕ} (h : ChainSet a k) : ChainSet a (k / 2)

theorem DescriptiveComplexity.chainSet_le {a k : ℕ} (h : ChainSet a k) : k ≤ a

theorem DescriptiveComplexity.chainSet_half_of_ne {a k : ℕ} (h : ChainSet a k) (hne : k ≠ a) : ChainSet (a / 2) k

Every entry but the top is an entry of the chain of the half.

theorem DescriptiveComplexity.chainSet_of_half {a k : ℕ} (h : ChainSet (a / 2) k) : ChainSet a k

…and conversely.

theorem DescriptiveComplexity.chainSet_le_half_of_lt {a k l : ℕ} (hk : ChainSet a k) (hl : ChainSet a l) (hlt : l < k) : l ≤ k / 2

The chain has no gaps: an entry below k is at most k / 2, so the predecessor of k in the chain is k / 2 – which is what lets a formula state the recursion for consecutive positions only.

Soundness: the chain conditions pin the exponents

theorem DescriptiveComplexity.val_eq_of_chain {S : ℕ → Prop} {val : ℕ → ℕ} (h0 : val 0 = 0) (hstep : ∀ (k : ℕ), S k → 0 < k → S (k / 2) ∧ val k = 2 * val (k / 2) + k % 2) (k : ℕ) : S k → val k = k

The certificate is sound: if a value is carried at every entry of a set containing 0, the value at 0 is 0, and each entry's value is twice its half's plus its own parity, then the value at every entry is that entry.

This is the whole of the soundness half of DescriptiveComplexity.PowArithDef, with the formula stripped away: val k is the field a guessed element carries at the position of index k, the parity is which of q' = q * q and q' = 2 * (q * q) fired, and the conclusion says the guess describes the exponents it claims to.

The layout: why the fields fit

theorem DescriptiveComplexity.half_add_size_le (k : ℕ) : k / 2 + (k / 2).size ≤ k

A value fits in its own number of bits, and a field of that width at position k / 2 never reaches k: Nat.size is the width, Nat.lt_size_self says the value fits, and this says the fields of a certificate are pairwise disjoint – the completeness half's only capacity condition.

The certificate's first element

@[irreducible]

def DescriptiveComplexity.chainBelow (a : ℕ) : ℕ

The chain below its top, as a number: one bit at the position of each a / 2 ^ t for t ≥ 1. This is the element Y a certificate guesses.

Equations

• DescriptiveComplexity.chainBelow a = if a = 0 then 0 else 2 ^ (a / 2) + DescriptiveComplexity.chainBelow (a / 2)

theorem DescriptiveComplexity.chainBelow_zero : chainBelow 0 = 0

theorem DescriptiveComplexity.chainBelow_pos {a : ℕ} (ha : 0 < a) : chainBelow a = 2 ^ (a / 2) + chainBelow (a / 2)

theorem DescriptiveComplexity.chainBelow_lt (a : ℕ) : chainBelow a < 2 ^ a

The chain below its top fits under its top: Y is a rank whenever the place value it certifies is one, which is what makes the certificate exist. The chain including its top need not fit, which is why the top is left out.

theorem DescriptiveComplexity.testBit_two_pow_add {m y : ℕ} (hy : y < 2 ^ m) (k : ℕ) : (2 ^ m + y).testBit k = if k < m then y.testBit k else decide (k = m)

A bit above a place value: with a low part below 2 ^ m, the bits of 2 ^ m + y are those of y below m, a one at m, and nothing above. This is the only bit-level computation the chain's element needs.

theorem DescriptiveComplexity.testBit_chainBelow (a k : ℕ) : (chainBelow a).testBit k = true ↔ ChainSet a k ∧ k ≠ a

The chain, read off its element: the bits of DescriptiveComplexity.chainBelow are exactly the entries of the chain other than its top – the top being the given place value, which is why it is left out.

The certificate's second element

@[irreducible]

def DescriptiveComplexity.chainVals (a : ℕ) : ℕ

The exponents of the chain, packed side by side: each entry below the top carries its own value in the field that starts at it and ends at the next entry. This is the element E a certificate guesses.

Equations

• DescriptiveComplexity.chainVals a = if a = 0 then 0 else a / 2 * 2 ^ (a / 2) + DescriptiveComplexity.chainVals (a / 2)

theorem DescriptiveComplexity.chainVals_zero : chainVals 0 = 0

theorem DescriptiveComplexity.chainVals_pos {a : ℕ} (ha : 0 < a) : chainVals a = a / 2 * 2 ^ (a / 2) + chainVals (a / 2)

theorem DescriptiveComplexity.half_lt_two_pow_sub (k : ℕ) : k / 2 < 2 ^ (k - k / 2)

An entry fits in the field it is given: k / 2 is written in the k - k / 2 bits between the positions of index k / 2 and k, which is DescriptiveComplexity.half_add_size_le read as a bound.

theorem DescriptiveComplexity.chainVals_lt (a : ℕ) : chainVals a < 2 ^ a

The packed exponents fit under the top place value: E is a rank whenever 2 ^ a is one, the top entry being the only one with no field.

theorem DescriptiveComplexity.exists_chainSucc {a k : ℕ} (hk : ChainSet a k) (hne : k ≠ a) : ∃ (l : ℕ), ChainSet a l ∧ 0 < l ∧ l / 2 = k

The chain, one step below a given entry: an entry other than the top has a next entry, and it is that entry's half.

theorem DescriptiveComplexity.chainVals_field (a l : ℕ) : ChainSet a l → 0 < l → chainVals a / 2 ^ (l / 2) % 2 ^ (l - l / 2) = l / 2

The layout works: between an entry and the next one, the packed element carries that entry. This is the whole completeness half of the field reading – the formula reads DescriptiveComplexity.FieldAt, and this says what it finds in the element the certificate builds.

The certificate, as a property of four elements

def DescriptiveComplexity.InChain {A : Type} [LinearOrder A] (p Y q : A) : Prop

The chain, as a set of elements: the given place value p – its top, which is not written into the guess – together with the positions marked in the guessed element Y.

Equations

• DescriptiveComplexity.InChain p Y q = (q = p ∨ DescriptiveComplexity.IsPos q ∧ DescriptiveComplexity.BitAt q Y)

def DescriptiveComplexity.ConsChain {A : Type} [LinearOrder A] (p Y q q' : A) : Prop

Two consecutive entries of the chain: nothing of the chain lies between them. DescriptiveComplexity.chainSet_le_half_of_lt is why speaking of consecutive entries is enough – the entry below k is k / 2.

Equations

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

def DescriptiveComplexity.ValAt {A : Type} [LinearOrder A] (i p Y E q v : A) : Prop

The exponent carried at a chain entry: the given i at the top, and otherwise the field of E running from the entry up to the next one. The top carries no field – there is no room above it – which is the same fact as its having no next entry.

Equations

• DescriptiveComplexity.ValAt i p Y E q v = (q = p ∧ v = i ∨ ¬q = p ∧ ∃ (q' : A), DescriptiveComplexity.ConsChain p Y q q' ∧ DescriptiveComplexity.FieldAt q q' E v)

def DescriptiveComplexity.PowCert {A : Type} [LinearOrder A] (i p Y E : A) : Prop

The certificate for orank p = 2 ^ orank i: p is a position and the greatest entry of the chain it tops; the chain's least entry is the place value 1, carrying the exponent 0; and consecutive entries square, or square and double, with their exponents doubling, or doubling and gaining one.

Equations

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

theorem DescriptiveComplexity.InChain.isPos {A : Type} [LinearOrder A] {p Y q : A} (h : InChain p Y q) (hp : IsPos p) : IsPos q

Every entry of the chain is a position, the top because it is assumed to be one.

theorem DescriptiveComplexity.posExp_lt_posExp {A : Type} [LinearOrder A] [Finite A] {q q' : A} (hq : IsPos q) (hq' : IsPos q') (h : q < q') : posExp q < posExp q'

Positions are ordered by their exponents.

theorem DescriptiveComplexity.consChain_unique {A : Type} [LinearOrder A] {p Y q q₁ q₂ : A} (h₁ : ConsChain p Y q q₁) (h₂ : ConsChain p Y q q₂) : q₁ = q₂

An entry has at most one next entry.

theorem DescriptiveComplexity.valAt_unique {A : Type} [LinearOrder A] [Finite A] {i p Y E q v v' : A} (hp : IsPos p) (h : ValAt i p Y E q v) (h' : ValAt i p Y E q v') : v = v'

An entry carries one exponent: at the top it is the given i, and elsewhere the field is a function of its two ends.

theorem DescriptiveComplexity.exists_consChain {A : Type} [LinearOrder A] [Finite A] {p Y q : A} (hq : InChain p Y q) (hlt : q < p) : ∃ (q' : A), ConsChain p Y q q'

Below the top there is a next entry: the least entry above the given one.

theorem DescriptiveComplexity.exists_consChain_lt {A : Type} [LinearOrder A] [Finite A] {p Y q r : A} (hq : InChain p Y q) (hr : InChain p Y r) (hlt : r < q) : ∃ (r' : A), ConsChain p Y r' q

Above the least entry there is a previous one: the greatest entry below the given one.

theorem DescriptiveComplexity.exists_valAt {A : Type} [LinearOrder A] [Finite A] {i p Y E q : A} (hp : IsPos p) (hmax : ∀ (r : A), InChain p Y r → r ≤ p) (hq : InChain p Y q) : ∃ (v : A), ValAt i p Y E q v

Every entry carries a value: the top the given i, and any other the field below its next entry, which is a rank because a field always is (DescriptiveComplexity.exists_fieldAt).

Soundness: what a certificate forces

noncomputable def DescriptiveComplexity.powVal {A : Type} [LinearOrder A] (i p Y E : A) (k : ℕ) : ℕ

The exponent a certificate carries at the position of index k: the value read at the unique position of that place value, and 0 where there is none. DescriptiveComplexity.valAt_unique is what makes this a function.

Equations

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

theorem DescriptiveComplexity.powVal_eq {A : Type} [LinearOrder A] [Finite A] {i p Y E q v : A} {k : ℕ} (hp : IsPos p) (hq : orank q = 2 ^ k) (hv : ValAt i p Y E q v) : powVal i p Y E k = orank v

theorem DescriptiveComplexity.powCert_sound {A : Type} [LinearOrder A] [Finite A] {i p Y E : A} (h : PowCert i p Y E) : orank p = 2 ^ orank i

A certificate is sound: whatever is guessed, the chain conditions force the value at each entry to be that entry's exponent, and the value at the top is the given i. Nothing is assumed about the layout of the fields – a garbage guess simply fails the conditions.

Completeness: the certificate exists

theorem DescriptiveComplexity.powCert_complete {A : Type} [LinearOrder A] [Finite A] {i p : A} (h : orank p = 2 ^ orank i) : ∃ (Y : A) (E : A), PowCert i p Y E

A certificate exists: the chain below the top is the element Y (DescriptiveComplexity.chainBelow), the exponents packed in its fields are the element E (DescriptiveComplexity.chainVals), and both are ranks because both are below the place value 2 ^ orank i that is assumed to be one.

theorem DescriptiveComplexity.powCert_iff {A : Type} [LinearOrder A] [Finite A] (i p : A) : (∃ (Y : A) (E : A), PowCert i p Y E) ↔ orank p = 2 ^ orank i

The certificate is exactly right: p is the place value of i if and only if the two elements can be guessed. This is the mathematics of DescriptiveComplexity.PowArithDef; what remains is to write the conditions as a formula.

The formula

theorem DescriptiveComplexity.arithDef_inChain {L : FirstOrder.Language} {α : Type} (p Y q : α) : ArithDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (v : α → x) => InChain (v p) (v Y) (v q)

The chain is first-order: an equality, a position test and a bit.

theorem DescriptiveComplexity.arithDef_consChain {L : FirstOrder.Language} {α : Type} (p Y q q' : α) : ArithDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (v : α → x) => ConsChain (v p) (v Y) (v q) (v q')

Consecutiveness is first-order: one universal quantifier says that nothing of the chain lies between.

theorem DescriptiveComplexity.arithDef_valAt {L : FirstOrder.Language} {α : Type} (i p Y E q m : α) : ArithDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (v : α → x) => ValAt (v i) (v p) (v Y) (v E) (v q) (v m)

The value at an entry is first-order: the given i at the top, and otherwise the field below the next entry (DescriptiveComplexity.arithDef_fieldAt).

theorem DescriptiveComplexity.arithDef_powCert {L : FirstOrder.Language} {α : Type} (i p Y E : α) : ArithDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (v : α → x) => PowCert (v i) (v p) (v Y) (v E)

The certificate is first-order: four conditions, none of them about the layout of the fields.

theorem DescriptiveComplexity.powArithDef (L : FirstOrder.Language) : PowArithDef L

The naming bridge, proved: the graph of i ↦ 2 ^ i is a formula of FO(≤, +, ×), so the index naming of the bit positions costs the logic nothing after all. This is Immerman 1999 Thm 1.17(2), and it is the half of Immerman's mutual definability that turns the machine model's logic FO(≤, BIT) into a fragment of FO(≤, +, ×).

The formula guesses two elements – the doubling chain below p, and its exponents packed into the fields the chain delimits – and states three conditions on them; DescriptiveComplexity.powCert_iff is that this is exactly right.