FO(≤, +, ×) into the bit logic: the machine model is AC⁰

The machine model of DescriptiveComplexity.LogTime is the logic FO(≤, BIT) and sits inside FO(≤, +, ×) (DescriptiveComplexity.LTDecidable.ac0Definable, through DescriptiveComplexity.powArithDef). This file is the other direction, FO(≤, +, ×) ⊆ FO(≤, +, BIT), and with it the equality:

Every DescriptiveComplexity.ArithDef relation is DescriptiveComplexity.BitDef (DescriptiveComplexity.ArithDef.bitDef), every AC⁰-definable problem is decided by a logarithmic-time machine with constantly many alternations (DescriptiveComplexity.AC0Definable.ltDecidable), and the two notions coincide (DescriptiveComplexity.ac0Definable_iff_ltDecidable).

The one atom the translation turns on – multiplication of ranks in the bit logic, DescriptiveComplexity.TimesBitDef – is the whole of Immerman 1999 Thm 1.17(1): the Bit Sum Lemma (DescriptiveComplexity.BitSum.PopAll, LogTime/BitSum/Level1.lean) and the column-wise multiplication built on it (DescriptiveComplexity.BitSum.bitDef_times, LogTime/BitSum/Times.lean). It is proved here as DescriptiveComplexity.timesBitDef, so nothing below carries a hypothesis: with DescriptiveComplexity.ltDecidable_iff_bitDefinable on the machine side, the machine model is exactly AC⁰.

How the induction goes

By recursion on FirstOrder.Language.BoundedFormula, with the free variables of a formula with n bound ones carried as α ⊕ Fin n – the layout the BitDef quantifiers already use. Three points, none of them deep, and all of them already paid for elsewhere in the library:

• Terms are variables. Both vocabularies are relational, so DescriptiveComplexity.relVar reads a term as the variable it is; this is why that definition sits in DescriptiveComplexity.ArithmeticDefinable, below both this file and the head-program evaluator that also needs it.
• The atom splits four ways, on the relation symbol: an input relation, ≤, plus and times, each bit-definable. It is the same four-way split as DescriptiveComplexity.HeadEvalArith, at the level of the logic instead of the machine.
• The quantifier is peelVar, the relabeling that moves the innermost bound variable out of the block and into the Fin 1 a BitDef quantifier binds, with DescriptiveComplexity.elim_comp_peelVar saying that this is Fin.snoc on valuations. DescriptiveComplexity.arithDef_prefixHolds does the same thing for the other logic.

What this is not

It is not a normal-form theorem: the bit logic is prenex by construction and the BitDef API merges prefixes semantically, so no toPrenex is involved.

The last atom

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

Multiplication of ranks, in the bit logic: the one atom of FO(≤, +, ×) that DescriptiveComplexity.BitDef does not have as a primitive, and hence the whole content of Immerman 1999 Thm 1.17(1) – the Bit Sum Lemma and the column-wise multiplication over it.

It is a named statement, uniformly in the variable layout, so that what it buys is visible in a type: the same discipline DescriptiveComplexity.PowArithDef follows, and the reason the two halves of Thm 1.17 can be compared at a glance.

Equations

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

theorem DescriptiveComplexity.timesBitDef {L : FirstOrder.Language} : TimesBitDef L

The last atom, proved: the certificate of LogTime/BitSum/Times.lean – column counts by the Bit Sum Lemma, one carry chain per block, an even and an odd packing and a tail – in the shape the translation consumes.

The translation

theorem DescriptiveComplexity.elim_proj {α A : Type} {n : ℕ} (u : α ⊕ Fin n → A) : (Sum.elim (fun (a : α) => u (Sum.inl a)) fun (i : Fin n) => u (Sum.inr i)) = u

Splitting a valuation of α ⊕ Fin n into its two halves and putting it back is the identity – the one bookkeeping step the atom cases need.

theorem DescriptiveComplexity.bitDef_realize {L : FirstOrder.Language} [L.IsRelational] {α : Type} {n : ℕ} (φ : (L.sum FirstOrder.Language.arith).BoundedFormula α n) : BitDef fun (x : Type) (x_1 : L.Structure x) (x_2 : LinearOrder x) (x_3 : Finite x) (x_4 : Nonempty x) (u : α ⊕ Fin n → x) => φ.Realize (fun (a : α) => u (Sum.inl a)) fun (i : Fin n) => u (Sum.inr i)

Every formula of FO(≤, +, ×) is bit-definable: the induction over FirstOrder.Language.BoundedFormula, with the bound variables carried as the right-hand summand of the variable type.

theorem DescriptiveComplexity.ArithDef.bitDef {L : FirstOrder.Language} [L.IsRelational] {α : Type} {R : ArithRel L α} (h : ArithDef R) : BitDef R

The two definability notions agree on relations: a formula of the arithmetic expansion becomes a sentence of the bit logic with the same free variables.

What it buys

theorem DescriptiveComplexity.AC0Definable.bitDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : AC0Definable P) : BitDefinable P

AC⁰ definability is bit-definability.

theorem DescriptiveComplexity.AC0Definable.ltDecidable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : AC0Definable P) : LTDecidable P

An AC⁰ definition is a logarithmic-time machine with constantly many alternations: the direction of Immerman's identification that the Bit Sum Lemma is the whole of.

theorem DescriptiveComplexity.ac0Definable_iff_ltDecidable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} : AC0Definable P ↔ LTDecidable P

AC⁰ is constant-alternation logarithmic time – the statement the whole DescriptiveComplexity.LogTime development aims at, with ⊇ through DescriptiveComplexity.powArithDef and ⊆ through DescriptiveComplexity.timesBitDef: both halves of Immerman 1999 Thm 1.17, with no hypothesis left.