The bit-level logic is inside LOGSPACE

DescriptiveComplexity.BitDefinable.mem_LOGSPACE: every problem defined by a prenex sentence over ≤, + and the bit at an index – hence, by DescriptiveComplexity.ltDecidable_iff_bitDefinable, every problem decided by an alternating machine with a logarithmic clock – is decided by a deterministic multi-head automaton, so it is in LOGSPACE.

This is the fence the index naming cost, restored without either half of Immerman's mutual definability: nothing here goes through FO(≤, +, ×), so this route is independent of DescriptiveComplexity.powArithDef.

Why it is short

The bit logic is prenex, so there is no formula induction to redo: the evaluator is a recursion over DescriptiveComplexity.BitKernel, whose five constructors become branches (DescriptiveComplexity.HeadProgram.iteP), and a quantifier prefix, whose variables become sweeps (DescriptiveComplexity.HeadProgram.scanP for a universal register, its negation for an existential). The prefix peels its innermost variable first, which is exactly how a sweep wraps a body, so the induction matches the semantics step for step and the property a prefix decides depends on no head at all.

Only the atoms have content, and all of it is elsewhere: ≤ and an input relation are quantifier-free guards, + is DescriptiveComplexity.HeadProgram.plusP, and the bit is DescriptiveComplexity.HeadProgram.bitP – the halving loop of DescriptiveComplexity.HeadBit.

The head budget

2 * vars + 8: two heads per quantified variable, the register itself and the sweep's marker, then the eight the bit fragment needs (its five working heads and the addition's three). Where an arithmetic evaluation pays seven scratch heads (DescriptiveComplexity.HeadProgram.ArithScratch), a bit-level one pays eight, and it never needs a multiplication.

Negating a fragment

def DescriptiveComplexity.HeadProgram.notP {L : FirstOrder.Language} {K : ℕ} (F : HeadProgram L K) : HeadProgram L K

The negation of a fragment: run it and swap the exits.

Equations

• F.notP = F.iteP (DescriptiveComplexity.HeadProgram.exitP false) (DescriptiveComplexity.HeadProgram.exitP true)

theorem DescriptiveComplexity.HeadProgram.decides_notP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} {F : HeadProgram L K} {P : (Fin K → A) → Prop} (hF : F.Decides A m P) (hP : HeadLocal m P) : F.notP.Decides A m fun (x : Fin K → A) => ¬P x

theorem DescriptiveComplexity.HeadProgram.deterministic_notP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {F : HeadProgram L K} (hF : F.Deterministic A) : F.notP.Deterministic A

The scratch layout of a bit-level evaluation

structure DescriptiveComplexity.HeadProgram.BitScratch {K : ℕ} (y cnt cand w tmk a b mk : Fin K) (S : ℕ) : Prop

The eight heads a bit-level atom needs, pinned to the eight positions from S on: the bit fragment's five working heads, then the addition's three. S is the top of the quantifier region, so every level the evaluator reaches is at most S.

• hy : ↑y = S

  The working value sits at S.

• hcnt : ↑cnt = S + 1

  The round counter sits at S + 1.

• hcand : ↑cand = S + 2

  The scan's candidate sits at S + 2.

• hw : ↑w = S + 3

  The candidate's successor sits at S + 3.

• htmk : ↑tmk = S + 4

  The scan's marker sits at S + 4.

• ha : ↑a = S + 5

  The addition's running head sits at S + 5.

• hb : ↑b = S + 6

  The addition's counter sits at S + 6.

• hmk : ↑mk = S + 7

  The addition's marker sits at S + 7.

The atoms

@[reducible, inline]

abbrev DescriptiveComplexity.HeadProgram.inOrdSym {L : FirstOrder.Language} {a : ℕ} (R : L.Relations a) : (L.sum FirstOrder.Language.order).Relations a

An input relation symbol, in the ordered expansion of its vocabulary. Named, as every symbol of a sum vocabulary in this library is, so that rw matches it.

Equations

• DescriptiveComplexity.HeadProgram.inOrdSym R = Sum.inl R

noncomputable def DescriptiveComplexity.HeadProgram.bitAtomP {L : FirstOrder.Language} {K : ℕ} (y cnt cand w tmk a b mk : Fin K) {γ : Type} (hv : γ → Fin K) : BitAtom L γ → HeadProgram L K

A bit-level atom, as a program: the order and an input relation are read as guards, the addition and the bit are computed, by plusP and by the halving loop bitP.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.bitAtomP y cnt cand w tmk a b mk hv (DescriptiveComplexity.BitAtom.le u v) = DescriptiveComplexity.HeadProgram.leafP (DescriptiveComplexity.leF (hv u) (hv v)) ⋯
• DescriptiveComplexity.HeadProgram.bitAtomP y cnt cand w tmk a b mk hv (DescriptiveComplexity.BitAtom.plus u v z) = DescriptiveComplexity.HeadProgram.plusP (hv u) (hv v) (hv z) a b mk
• DescriptiveComplexity.HeadProgram.bitAtomP y cnt cand w tmk a b mk hv (DescriptiveComplexity.BitAtom.bit u v) = DescriptiveComplexity.HeadProgram.bitP (hv u) (hv v) y cnt cand w tmk a b mk

noncomputable def DescriptiveComplexity.HeadProgram.bitKernelP {L : FirstOrder.Language} {K : ℕ} (y cnt cand w tmk a b mk : Fin K) {γ : Type} (hv : γ → Fin K) : BitKernel L γ → HeadProgram L K

The quantifier-free kernel, as a program: the Boolean structure becomes branches.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.bitKernelP y cnt cand w tmk a b mk hv (DescriptiveComplexity.BitKernel.atom at') = DescriptiveComplexity.HeadProgram.bitAtomP y cnt cand w tmk a b mk hv at'
• DescriptiveComplexity.HeadProgram.bitKernelP y cnt cand w tmk a b mk hv DescriptiveComplexity.BitKernel.tt = DescriptiveComplexity.HeadProgram.exitP true
• DescriptiveComplexity.HeadProgram.bitKernelP y cnt cand w tmk a b mk hv k.not = (DescriptiveComplexity.HeadProgram.bitKernelP y cnt cand w tmk a b mk hv k).notP

noncomputable def DescriptiveComplexity.HeadProgram.quantP {L : FirstOrder.Language} {K : ℕ} (pol : Bool) (h hm : Fin K) (F : HeadProgram L K) : HeadProgram L K

A quantified register, as a sweep: universally the sweep itself, and existentially its double negation.

Equations

• DescriptiveComplexity.HeadProgram.quantP pol h hm F = if pol = true then (DescriptiveComplexity.HeadProgram.scanP h hm F.notP).notP else DescriptiveComplexity.HeadProgram.scanP h hm F

noncomputable def DescriptiveComplexity.HeadProgram.prefixP {L : FirstOrder.Language} {K : ℕ} (sh : ℕ → Fin K) (n : ℕ) : (Fin n → Bool) → HeadProgram L K → HeadProgram L K

The quantifier prefix, as nested sweeps: the innermost variable wraps the body first, which is how DescriptiveComplexity.prefixHolds peels it. Variable j lives in head sh (2 * j), its sweep's marker in sh (2 * j + 1).

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HeadProgram.prefixP sh 0 x_3 x✝ = x✝

Correctness

Determinism

theorem DescriptiveComplexity.HeadProgram.deterministic_bitAtomP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {y cnt cand w tmk a b mk : Fin K} {γ : Type} (hv : γ → Fin K) (at' : BitAtom L γ) : (bitAtomP y cnt cand w tmk a b mk hv at').Deterministic A

theorem DescriptiveComplexity.HeadProgram.deterministic_bitKernelP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {y cnt cand w tmk a b mk : Fin K} {γ : Type} (hv : γ → Fin K) (k : BitKernel L γ) : (bitKernelP y cnt cand w tmk a b mk hv k).Deterministic A

theorem DescriptiveComplexity.HeadProgram.deterministic_quantP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {pol : Bool} {h hm : Fin K} {F : HeadProgram L K} (hF : F.Deterministic A) : (quantP pol h hm F).Deterministic A

theorem DescriptiveComplexity.HeadProgram.deterministic_prefixP {L : FirstOrder.Language} {K : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (sh : ℕ → Fin K) (n : ℕ) (pol : Fin n → Bool) (F : HeadProgram L K) : F.Deterministic A → (prefixP sh n pol F).Deterministic A

The inclusion

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

The bit-level logic is inside FO(DTC): a prenex sentence over ≤, + and the bit at an index is evaluated by a deterministic multi-head automaton – the registers swept, the order and the input atoms read as guards, the addition and the bit computed by DescriptiveComplexity.HeadProgram.plusP and DescriptiveComplexity.HeadProgram.bitP.

The machine has 2 * vars + 8 heads: two per quantified register, then the eight the bit fragment needs.

theorem DescriptiveComplexity.BitDefinable.mem_LOGSPACE {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : BitDefinable P) : LOGSPACE.Mem P

The bit-level logic is inside LOGSPACE, and with it the machine model of DescriptiveComplexity.LogTime. No part of Immerman's mutual definability is used: the route through AC⁰ (DescriptiveComplexity.powArithDef, then DescriptiveComplexity.ac0Definable_mem_LOGSPACE) is a different one, and longer.

theorem DescriptiveComplexity.LTDecidable.mem_LOGSPACE {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : LTDecidable P) : LOGSPACE.Mem P

Constant-alternation logarithmic time is inside LOGSPACE, through the logic it is equal to.