The Σₖ kernel of alternating acceptance

The first-order kernel the k second-order blocks of the membership proof sit under. It is the kernel of DescriptiveComplexity.Problems.Machine.Membership – the same seventeen clauses, transcribing the same relations – with three differences:

• the vocabulary is DescriptiveComplexity.akLang, the alternating machine's together with the merged block of k copies of the guessing block, so a clause names the round whose run it speaks of (DescriptiveComplexity.akSt and friends, read back by DescriptiveComplexity.relMap_akSt);
• the block marks are read as finite disjunctions over Fin k, which is what makes “the state at this time is in a block below i” first-order;
• the clauses are assembled not into a conjunction but into the alternating chain DescriptiveComplexity.akLadderF, matching the matrix of DescriptiveComplexity.Problems.Machine.AltMatrix.

Every builder here is parameterized by the round it reads, so the file writes the clause layer once rather than k times.

The vocabulary of the kernel

@[reducible, inline]

abbrev DescriptiveComplexity.akLang (k : ℕ) : FirstOrder.Language

The vocabulary of the kernel: the alternating machine's, expanded by the merged block of one guessed run per round.

Equations

• DescriptiveComplexity.akLang k = (FirstOrder.Language.turingAlt k).sum (DescriptiveComplexity.repMerged DescriptiveComplexity.tmGuessBlock k).lang

@[reducible, inline]

abbrev DescriptiveComplexity.akPosnSym {k : ℕ} : (akLang k).Relations 1

The position symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.akPosnSym = Sum.inl FirstOrder.Language.atmPosn

@[reducible, inline]

abbrev DescriptiveComplexity.akTrSym {k : ℕ} : (akLang k).Relations 1

The transition symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.akTrSym = Sum.inl FirstOrder.Language.atmTr

@[reducible, inline]

abbrev DescriptiveComplexity.akStartSym {k : ℕ} : (akLang k).Relations 1

The start-state symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.akStartSym = Sum.inl FirstOrder.Language.atmStart

@[reducible, inline]

abbrev DescriptiveComplexity.akAccSym {k : ℕ} : (akLang k).Relations 1

The accepting-state symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.akAccSym = Sum.inl FirstOrder.Language.atmAcc

@[reducible, inline]

abbrev DescriptiveComplexity.akBlankSym {k : ℕ} : (akLang k).Relations 1

The blank symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.akBlankSym = Sum.inl FirstOrder.Language.atmBlank

@[reducible, inline]

abbrev DescriptiveComplexity.akRightSym {k : ℕ} : (akLang k).Relations 1

The move-right symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.akRightSym = Sum.inl FirstOrder.Language.atmRight

@[reducible, inline]

abbrev DescriptiveComplexity.akLeSym {k : ℕ} : (akLang k).Relations 2

The order symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.akLeSym = Sum.inl FirstOrder.Language.atmLe

@[reducible, inline]

abbrev DescriptiveComplexity.akSrcSym {k : ℕ} : (akLang k).Relations 2

The source symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.akSrcSym = Sum.inl FirstOrder.Language.atmSrc

@[reducible, inline]

abbrev DescriptiveComplexity.akReadSym {k : ℕ} : (akLang k).Relations 2

The read symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.akReadSym = Sum.inl FirstOrder.Language.atmRead

@[reducible, inline]

abbrev DescriptiveComplexity.akDstSym {k : ℕ} : (akLang k).Relations 2

The target symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.akDstSym = Sum.inl FirstOrder.Language.atmDst

@[reducible, inline]

abbrev DescriptiveComplexity.akWriteSym {k : ℕ} : (akLang k).Relations 2

The write symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.akWriteSym = Sum.inl FirstOrder.Language.atmWrite

@[reducible, inline]

abbrev DescriptiveComplexity.akInpSym {k : ℕ} : (akLang k).Relations 2

The input symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.akInpSym = Sum.inl FirstOrder.Language.atmInp

@[reducible, inline]

abbrev DescriptiveComplexity.akBlkSym {k : ℕ} (j : Fin k) : (akLang k).Relations 1

The mark of block j in the kernel's vocabulary.

Equations

• DescriptiveComplexity.akBlkSym j = Sum.inl (FirstOrder.Language.atmBlk j)

def DescriptiveComplexity.akSt {k : ℕ} (i : Fin k) : (akLang k).Relations 2

The state variable of round i.

Equations

• DescriptiveComplexity.akSt i = Sum.inr (DescriptiveComplexity.repSym DescriptiveComplexity.tmGuessBlock DescriptiveComplexity.TMIdx.state DescriptiveComplexity.akSt._proof_1 k i)

def DescriptiveComplexity.akHd {k : ℕ} (i : Fin k) : (akLang k).Relations 2

The head variable of round i.

Equations

• DescriptiveComplexity.akHd i = Sum.inr (DescriptiveComplexity.repSym DescriptiveComplexity.tmGuessBlock DescriptiveComplexity.TMIdx.head DescriptiveComplexity.akHd._proof_1 k i)

def DescriptiveComplexity.akTp {k : ℕ} (i : Fin k) : (akLang k).Relations 3

The tape variable of round i.

Equations

• DescriptiveComplexity.akTp i = Sum.inr (DescriptiveComplexity.repSym DescriptiveComplexity.tmGuessBlock DescriptiveComplexity.TMIdx.tape DescriptiveComplexity.akTp._proof_1 k i)

Formula builders

def DescriptiveComplexity.akPosnF {k : ℕ} {α : Type} (x : α) : (akLang k).Formula α

x is a position, as a formula.

Equations

• DescriptiveComplexity.akPosnF x = DescriptiveComplexity.akPosnSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.akTrF {k : ℕ} {α : Type} (x : α) : (akLang k).Formula α

x is a transition, as a formula.

Equations

• DescriptiveComplexity.akTrF x = DescriptiveComplexity.akTrSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.akStartF {k : ℕ} {α : Type} (x : α) : (akLang k).Formula α

x is a start state, as a formula.

Equations

• DescriptiveComplexity.akStartF x = DescriptiveComplexity.akStartSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.akAccF {k : ℕ} {α : Type} (x : α) : (akLang k).Formula α

x is an accepting state, as a formula.

Equations

• DescriptiveComplexity.akAccF x = DescriptiveComplexity.akAccSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.akBlankF {k : ℕ} {α : Type} (x : α) : (akLang k).Formula α

x is the blank symbol, as a formula.

Equations

• DescriptiveComplexity.akBlankF x = DescriptiveComplexity.akBlankSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.akRightF {k : ℕ} {α : Type} (x : α) : (akLang k).Formula α

x moves the head right, as a formula.

Equations

• DescriptiveComplexity.akRightF x = DescriptiveComplexity.akRightSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.akBlkF {k : ℕ} {α : Type} (j : Fin k) (x : α) : (akLang k).Formula α

x carries the mark of block j, as a formula.

Equations

• DescriptiveComplexity.akBlkF j x = (DescriptiveComplexity.akBlkSym j).formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.akLeF {k : ℕ} {α : Type} (x y : α) : (akLang k).Formula α

x ≤ y, as a formula.

Equations

• DescriptiveComplexity.akLeF x y = DescriptiveComplexity.akLeSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.akEqF {k : ℕ} {α : Type} (x y : α) : (akLang k).Formula α

x = y, as a formula.

Equations

• DescriptiveComplexity.akEqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

def DescriptiveComplexity.akSrcF {k : ℕ} {α : Type} (x y : α) : (akLang k).Formula α

The transition x applies in the state y, as a formula.

Equations

• DescriptiveComplexity.akSrcF x y = DescriptiveComplexity.akSrcSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.akReadF {k : ℕ} {α : Type} (x y : α) : (akLang k).Formula α

The transition x reads the symbol y, as a formula.

Equations

• DescriptiveComplexity.akReadF x y = DescriptiveComplexity.akReadSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.akDstF {k : ℕ} {α : Type} (x y : α) : (akLang k).Formula α

The transition x moves to the state y, as a formula.

Equations

• DescriptiveComplexity.akDstF x y = DescriptiveComplexity.akDstSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.akWriteF {k : ℕ} {α : Type} (x y : α) : (akLang k).Formula α

The transition x writes the symbol y, as a formula.

Equations

• DescriptiveComplexity.akWriteF x y = DescriptiveComplexity.akWriteSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.akInpF {k : ℕ} {α : Type} (x y : α) : (akLang k).Formula α

The cell x initially holds y, as a formula.

Equations

• DescriptiveComplexity.akInpF x y = DescriptiveComplexity.akInpSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.akStF {k : ℕ} {α : Type} (i : Fin k) (x y : α) : (akLang k).Formula α

In round i, the state at time x is y.

Equations

• DescriptiveComplexity.akStF i x y = (DescriptiveComplexity.akSt i).formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.akHdF {k : ℕ} {α : Type} (i : Fin k) (x y : α) : (akLang k).Formula α

In round i, the head at time x is on y.

Equations

• DescriptiveComplexity.akHdF i x y = (DescriptiveComplexity.akHd i).formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.akTpF {k : ℕ} {α : Type} (i : Fin k) (x y z : α) : (akLang k).Formula α

In round i, at time x the cell y holds z.

Equations

• DescriptiveComplexity.akTpF i x y z = (DescriptiveComplexity.akTp i).formula ![FirstOrder.Language.var x, FirstOrder.Language.var y, FirstOrder.Language.var z]

noncomputable def DescriptiveComplexity.akMinPosF {k : ℕ} {α : Type} (x : α) : (akLang k).Formula α

x is the lowest position, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.akMaxPosF {k : ℕ} {α : Type} (x : α) : (akLang k).Formula α

x is the highest position, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.akSuccPosF {k : ℕ} {α : Type} (x y : α) : (akLang k).Formula α

y is the position immediately above x, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.akInitTapeF {k : ℕ} {α : Type} (x y : α) : (akLang k).Formula α

The cell x may initially hold y.

Equations

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

noncomputable def DescriptiveComplexity.akBlkLeF {k : ℕ} {α : Type} (i : Fin k) (x : α) : (akLang k).Formula α

The state x is in a block at most i.

Equations

• DescriptiveComplexity.akBlkLeF i x = FirstOrder.Language.Formula.iSup fun (j : { j : Fin k // ↑j ≤ ↑i }) => DescriptiveComplexity.akBlkF (↑j) x

noncomputable def DescriptiveComplexity.akBlkLtF {k : ℕ} {α : Type} (i : Fin k) (t : α) : (akLang k).Formula α

In round i, the state at time t is in a block at most i – that is, in a block below i + 1.

Equations

• DescriptiveComplexity.akBlkLtF i t = FirstOrder.Language.Formula.iAlls (Fin 1) ((DescriptiveComplexity.akStF i (Sum.inl t) (Sum.inr 0)).imp (DescriptiveComplexity.akBlkLeF i (Sum.inr 0)))

noncomputable def DescriptiveComplexity.akAccAtF {k : ℕ} {α : Type} (i : Fin k) (t : α) : (akLang k).Formula α

In round i, the state at time t is accepting.

Equations

• DescriptiveComplexity.akAccAtF i t = FirstOrder.Language.Formula.iAlls (Fin 1) ((DescriptiveComplexity.akStF i (Sum.inl t) (Sum.inr 0)).imp (DescriptiveComplexity.akAccF (Sum.inr 0)))

noncomputable def DescriptiveComplexity.akMoveExF {k : ℕ} {α : Type} (i : Fin k) (t : α) (dir : Bool) : (akLang k).Formula α

In round i, the head at time t has somewhere to move in the direction dir.

Equations

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

noncomputable def DescriptiveComplexity.akMoveF {k : ℕ} {α : Type} (i : Fin k) (t t' : α) (dir : Bool) : (akLang k).Formula α

In round i, the head moves from its cell at t to its cell at t', in the direction dir.

Equations

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

noncomputable def DescriptiveComplexity.akAppBodyF {k : ℕ} {α : Type} (i : Fin k) (t τ : α) : (akLang k).Formula α

The applicable-transition body: the transition τ fires on the configuration of round i at time t.

Equations

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

noncomputable def DescriptiveComplexity.akAppTrF {k : ℕ} {α : Type} (i : Fin k) (t : α) : (akLang k).Formula α

In round i, some transition applies to the configuration at time t.

Equations

• DescriptiveComplexity.akAppTrF i t = FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.akAppBodyF i (Sum.inl t) (Sum.inr 0))

noncomputable def DescriptiveComplexity.akStepBodyF {k : ℕ} {α : Type} (i : Fin k) (t t' τ : α) : (akLang k).Formula α

The step body: in round i, the transition τ takes the configuration at t to the one at t'.

Equations

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

noncomputable def DescriptiveComplexity.akStepF {k : ℕ} {α : Type} (i : Fin k) (t t' : α) : (akLang k).Formula α

In round i, the configuration at t steps to the one at t'.

Equations

• DescriptiveComplexity.akStepF i t t' = FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.akStepBodyF i (Sum.inl t) (Sum.inl t') (Sum.inr 0))

noncomputable def DescriptiveComplexity.akSameF {k : ℕ} {α : Type} (i i' : Fin k) (t t' : α) : (akLang k).Formula α

The configuration of round i' at time t' is the one of round i at time t.

Equations

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

noncomputable def DescriptiveComplexity.akInitAtF {k : ℕ} {α : Type} (i : Fin k) (t : α) : (akLang k).Formula α

In round i, the configuration at time t is initial.

Equations

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

Realization of the builders

@[instance_reducible]

def DescriptiveComplexity.akStructure {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) : (akLang k).Structure A

The structure the kernel is read in: the instance expanded by one guessed run per round.

Equations

• DescriptiveComplexity.akStructure ρs = inferInstance

The guessed relations

theorem DescriptiveComplexity.relMap_akSt {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) (i : Fin k) (v : Fin 2 → A) : FirstOrder.Language.Structure.RelMap (akSt i) v ↔ ρs i TMIdx.state v

@[simp]

theorem DescriptiveComplexity.realize_akStF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (i : Fin k) (x y : α) : (akStF i x y).Realize v ↔ runQ (ρs i) (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_akHdF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (i : Fin k) (x y : α) : (akHdF i x y).Realize v ↔ runH (ρs i) (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_akTpF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (i : Fin k) (x y z : α) : (akTpF i x y z).Realize v ↔ runT (ρs i) (v x) (v y) (v z)

The machine relations

@[simp]

theorem DescriptiveComplexity.realize_akPosnF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (akPosnF x).Realize v ↔ (atmData k A).Posn (v x)

@[simp]

theorem DescriptiveComplexity.realize_akTrF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (akTrF x).Realize v ↔ (atmData k A).Tr (v x)

@[simp]

theorem DescriptiveComplexity.realize_akStartF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (akStartF x).Realize v ↔ (atmData k A).Start (v x)

@[simp]

theorem DescriptiveComplexity.realize_akAccF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (akAccF x).Realize v ↔ (atmData k A).Acc (v x)

@[simp]

theorem DescriptiveComplexity.realize_akBlankF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (akBlankF x).Realize v ↔ (atmData k A).Blank (v x)

@[simp]

theorem DescriptiveComplexity.realize_akRightF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (akRightF x).Realize v ↔ (atmData k A).Right (v x)

@[simp]

theorem DescriptiveComplexity.realize_akBlkF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (j : Fin k) (x : α) : (akBlkF j x).Realize v ↔ (atmData k A).Blk (↑j) (v x)

@[simp]

theorem DescriptiveComplexity.realize_akLeF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (akLeF x y).Realize v ↔ (atmData k A).Le (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_akEqF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (akEqF x y).Realize v ↔ v x = v y

@[simp]

theorem DescriptiveComplexity.realize_akSrcF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (akSrcF x y).Realize v ↔ (atmData k A).Src (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_akReadF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (akReadF x y).Realize v ↔ (atmData k A).Read (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_akDstF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (akDstF x y).Realize v ↔ (atmData k A).Dst (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_akWriteF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (akWriteF x y).Realize v ↔ (atmData k A).Write (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_akInpF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (akInpF x y).Realize v ↔ (atmData k A).Inp (v x) (v y)

The derived formulas

@[simp]

theorem DescriptiveComplexity.realize_akMinPosF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (akMinPosF x).Realize v ↔ MinPos (atmData k A).Le (atmData k A).Posn (v x)

@[simp]

theorem DescriptiveComplexity.realize_akMaxPosF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x : α) : (akMaxPosF x).Realize v ↔ MaxPos (atmData k A).Le (atmData k A).Posn (v x)

@[simp]

theorem DescriptiveComplexity.realize_akSuccPosF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (akSuccPosF x y).Realize v ↔ SuccPos (atmData k A).Le (atmData k A).Posn (v x) (v y)

@[simp]

theorem DescriptiveComplexity.realize_akInitTapeF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (x y : α) : (akInitTapeF x y).Realize v ↔ (atmData k A).Inp (v x) (v y) ∨ (∀ (b : A), ¬(atmData k A).Inp (v x) b) ∧ (atmData k A).Blank (v y)

@[simp]

theorem DescriptiveComplexity.realize_akBlkLeF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (i : Fin k) (x : α) : (akBlkLeF i x).Realize v ↔ (atmData k A).BlkLt (↑i + 1) (v x)

@[simp]

theorem DescriptiveComplexity.realize_akBlkLtF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (i : Fin k) (t : α) : (akBlkLtF i t).Realize v ↔ (atmData k A).RunBlkLt (ρs i) (↑i + 1) (v t)

@[simp]

theorem DescriptiveComplexity.realize_akAccAtF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (i : Fin k) (t : α) : (akAccAtF i t).Realize v ↔ (atmData k A).RunAcc (ρs i) (v t)

@[simp]

theorem DescriptiveComplexity.realize_akMoveExF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (i : Fin k) (t : α) (dir : Bool) : (akMoveExF i t dir).Realize v ↔ ∀ (p : A), runH (ρs i) (v t) p → ∃ (p' : A), if dir = true then SuccPos (atmData k A).Le (atmData k A).Posn p p' else SuccPos (atmData k A).Le (atmData k A).Posn p' p

@[simp]

theorem DescriptiveComplexity.realize_akMoveF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (i : Fin k) (t t' : α) (dir : Bool) : (akMoveF i t t' dir).Realize v ↔ ∀ (p p' : A), runH (ρs i) (v t) p → runH (ρs i) (v t') p' → if dir = true then SuccPos (atmData k A).Le (atmData k A).Posn p p' else SuccPos (atmData k A).Le (atmData k A).Posn p' p

The composite formulas

@[simp]

theorem DescriptiveComplexity.realize_akAppBodyF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (i : Fin k) (t τ : α) : (akAppBodyF i t τ).Realize v ↔ (atmData k A).Tr (v τ) ∧ (∀ (q : A), runQ (ρs i) (v t) q → (atmData k A).Src (v τ) q) ∧ (∀ (p a : A), runH (ρs i) (v t) p → runT (ρs i) (v t) p a → (atmData k A).Read (v τ) a) ∧ (∃ (q : A), (atmData k A).Dst (v τ) q) ∧ (∃ (a : A), (atmData k A).Write (v τ) a) ∧ (((atmData k A).Right (v τ) ∧ ∀ (p : A), runH (ρs i) (v t) p → ∃ (p' : A), SuccPos (atmData k A).Le (atmData k A).Posn p p') ∨ ¬(atmData k A).Right (v τ) ∧ ∀ (p : A), runH (ρs i) (v t) p → ∃ (p' : A), SuccPos (atmData k A).Le (atmData k A).Posn p' p)

@[simp]

theorem DescriptiveComplexity.realize_akAppTrF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (i : Fin k) (t : α) : (akAppTrF i t).Realize v ↔ (atmData k A).RunAppTr (ρs i) (v t)

@[simp]

theorem DescriptiveComplexity.realize_akStepBodyF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (i : Fin k) (t t' τ : α) : (akStepBodyF i t t' τ).Realize v ↔ (atmData k A).Tr (v τ) ∧ (∀ (q : A), runQ (ρs i) (v t) q → (atmData k A).Src (v τ) q) ∧ (∀ (p a : A), runH (ρs i) (v t) p → runT (ρs i) (v t) p a → (atmData k A).Read (v τ) a) ∧ (∀ (q : A), runQ (ρs i) (v t') q → (atmData k A).Dst (v τ) q) ∧ (∀ (p a : A), runH (ρs i) (v t) p → runT (ρs i) (v t') p a → (atmData k A).Write (v τ) a) ∧ (∀ (p a : A), ¬runH (ρs i) (v t) p → (runT (ρs i) (v t) p a ↔ runT (ρs i) (v t') p a)) ∧ (((atmData k A).Right (v τ) ∧ ∀ (p p' : A), runH (ρs i) (v t) p → runH (ρs i) (v t') p' → SuccPos (atmData k A).Le (atmData k A).Posn p p') ∨ ¬(atmData k A).Right (v τ) ∧ ∀ (p p' : A), runH (ρs i) (v t) p → runH (ρs i) (v t') p' → SuccPos (atmData k A).Le (atmData k A).Posn p' p)

@[simp]

theorem DescriptiveComplexity.realize_akStepF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (i : Fin k) (t t' : α) : (akStepF i t t').Realize v ↔ (atmData k A).RunStep (v t) (v t')

@[simp]

theorem DescriptiveComplexity.realize_akSameF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (i i' : Fin k) (t t' : α) : (akSameF i i' t t').Realize v ↔ ATMData.RunSame (ρs i) (ρs i') (v t) (v t')

@[simp]

theorem DescriptiveComplexity.realize_akInitAtF {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) {α : Type} (v : α → A) (i : Fin k) (t : α) : (akInitAtF i t).Realize v ↔ (atmData k A).RunInit (ρs i) (v t)

The clauses

noncomputable def DescriptiveComplexity.akStateExClause {k : ℕ} (i : Fin k) : (akLang k).Sentence

In round i there is a state at each time.

Equations

• DescriptiveComplexity.akStateExClause i = FirstOrder.Language.Formula.iAlls (Fin 1) (FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.akStF i (Sum.inl (Sum.inr 0)) (Sum.inr 0)))

noncomputable def DescriptiveComplexity.akStateUniqClause {k : ℕ} (i : Fin k) : (akLang k).Sentence

In round i there is only one state at each time.

Equations

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

noncomputable def DescriptiveComplexity.akHeadExClause {k : ℕ} (i : Fin k) : (akLang k).Sentence

In round i the head is somewhere at each time.

Equations

• DescriptiveComplexity.akHeadExClause i = FirstOrder.Language.Formula.iAlls (Fin 1) (FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.akHdF i (Sum.inl (Sum.inr 0)) (Sum.inr 0)))

noncomputable def DescriptiveComplexity.akHeadUniqClause {k : ℕ} (i : Fin k) : (akLang k).Sentence

In round i the head is in only one place at each time.

Equations

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

noncomputable def DescriptiveComplexity.akTapeExClause {k : ℕ} (i : Fin k) : (akLang k).Sentence

In round i every cell holds a symbol at each time.

Equations

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

noncomputable def DescriptiveComplexity.akTapeUniqClause {k : ℕ} (i : Fin k) : (akLang k).Sentence

In round i every cell holds only one symbol at each time.

Equations

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

noncomputable def DescriptiveComplexity.akFunClause {k : ℕ} (i : Fin k) : (akLang k).Sentence

The guess of round i is functional.

Equations

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

noncomputable def DescriptiveComplexity.akInitClause {k : ℕ} (i : Fin k) : (akLang k).Sentence

In round i the configuration at the lowest time is initial.

Equations

• DescriptiveComplexity.akInitClause i = FirstOrder.Language.Formula.iAlls (Fin 1) ((DescriptiveComplexity.akMinPosF (Sum.inr 0)).imp (DescriptiveComplexity.akInitAtF i (Sum.inr 0)))

noncomputable def DescriptiveComplexity.akBlkMonoClause {k : ℕ} (i : Fin k) : (akLang k).Sentence

In round i the blocks never decrease.

Equations

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

noncomputable def DescriptiveComplexity.akStepClause {k : ℕ} (i : Fin k) : (akLang k).Sentence

In round i consecutive times step or stutter, as far as the round answers for them.

Equations

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

noncomputable def DescriptiveComplexity.akLegalClause {k : ℕ} (i : Fin k) : (akLang k).Sentence

The guess of round i is legal below block i + 1.

Equations

• DescriptiveComplexity.akLegalClause i = DescriptiveComplexity.akInitClause i ⊓ (DescriptiveComplexity.akBlkMonoClause i ⊓ DescriptiveComplexity.akStepClause i)

noncomputable def DescriptiveComplexity.akAgreeClause {k : ℕ} (j i : Fin k) : (akLang k).Sentence

Round i reproduces what round j committed.

Equations

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

noncomputable def DescriptiveComplexity.akAccClause {k : ℕ} (i : Fin k) : (akLang k).Sentence

The guess of round i accepts.

Equations

• DescriptiveComplexity.akAccClause i = FirstOrder.Language.Formula.iAlls (Fin 1) ((DescriptiveComplexity.akMaxPosF (Sum.inr 0)).imp (DescriptiveComplexity.akAccAtF i (Sum.inr 0)))

noncomputable def DescriptiveComplexity.akReflClause (k : ℕ) : (akLang k).Sentence

The order is reflexive.

Equations

• DescriptiveComplexity.akReflClause k = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.akLeF (Sum.inr 0) (Sum.inr 0))

noncomputable def DescriptiveComplexity.akTransClause (k : ℕ) : (akLang k).Sentence

The order is transitive.

Equations

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

noncomputable def DescriptiveComplexity.akAntisymClause (k : ℕ) : (akLang k).Sentence

The order is antisymmetric.

Equations

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

noncomputable def DescriptiveComplexity.akTotalClause (k : ℕ) : (akLang k).Sentence

The order is total.

Equations

• DescriptiveComplexity.akTotalClause k = FirstOrder.Language.Formula.iAlls (Fin 2) (DescriptiveComplexity.akLeF (Sum.inr 0) (Sum.inr 1) ⊔ DescriptiveComplexity.akLeF (Sum.inr 1) (Sum.inr 0))

noncomputable def DescriptiveComplexity.akPosnExClause (k : ℕ) : (akLang k).Sentence

There is a position.

Equations

• DescriptiveComplexity.akPosnExClause k = FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.akPosnF (Sum.inr 0))

noncomputable def DescriptiveComplexity.akInpFunClause (k : ℕ) : (akLang k).Sentence

The input is functional.

Equations

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

noncomputable def DescriptiveComplexity.akBlankExClause (k : ℕ) : (akLang k).Sentence

There is a blank symbol.

Equations

• DescriptiveComplexity.akBlankExClause k = FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.akBlankF (Sum.inr 0))

noncomputable def DescriptiveComplexity.akBlankUniqClause (k : ℕ) : (akLang k).Sentence

There is only one blank symbol.

Equations

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

noncomputable def DescriptiveComplexity.akWfClause (k : ℕ) : (akLang k).Sentence

The instance is a well-formed machine.

Equations

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

noncomputable def DescriptiveComplexity.akOneBlkClause (k : ℕ) : (akLang k).Sentence

Every state carries exactly one block mark.

Equations

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

noncomputable def DescriptiveComplexity.akStepBlkClause (k : ℕ) : (akLang k).Sentence

A transition stays in its block or moves to the next one.

Equations

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

noncomputable def DescriptiveComplexity.akStartBlkClause (k : ℕ) : (akLang k).Sentence

A start state is in block 0.

Equations

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

noncomputable def DescriptiveComplexity.akBwfClause (k : ℕ) : (akLang k).Sentence

The block structure is well formed.

Equations

• DescriptiveComplexity.akBwfClause k = DescriptiveComplexity.akOneBlkClause k ⊓ (DescriptiveComplexity.akStepBlkClause k ⊓ DescriptiveComplexity.akStartBlkClause k)

noncomputable def DescriptiveComplexity.akStartExClause (k : ℕ) : (akLang k).Sentence

There is a start state – the one existence clause of the game that is not redundant.

Equations

• DescriptiveComplexity.akStartExClause k = FirstOrder.Language.Formula.iExs (Fin 1) (DescriptiveComplexity.akStartF (Sum.inr 0))

Realization of the clauses

The ladder and the kernel

noncomputable def DescriptiveComplexity.polForm {k : ℕ} (pol : Bool) (φ ψ : (akLang k).Sentence) : (akLang k).Sentence

The connective a round of the ladder uses, as a formula: a conjunction where the round is existential, an implication where it is universal.

Equations

• DescriptiveComplexity.polForm true φ ψ = φ ⊓ ψ
• DescriptiveComplexity.polForm false φ ψ = FirstOrder.Language.Formula.imp φ ψ

noncomputable def DescriptiveComplexity.akRoundF {k : ℕ} (i : Fin k) (prev : Option (Fin k)) : (akLang k).Sentence

The condition round i puts on its guess: functional, legal, and – unless it is the first round – agreeing with the round before it.

Equations

• DescriptiveComplexity.akRoundF i none = DescriptiveComplexity.akFunClause i ⊓ DescriptiveComplexity.akLegalClause i
• DescriptiveComplexity.akRoundF i (some j) = DescriptiveComplexity.akFunClause i ⊓ (DescriptiveComplexity.akLegalClause i ⊓ DescriptiveComplexity.akAgreeClause j i)

noncomputable def DescriptiveComplexity.akLadderF (start : Bool) (k m i : ℕ) : i + m = k → Option (Fin k) → (akLang k).Sentence

The ladder, as a first-order sentence: the m rounds still to play from round i on, chained by DescriptiveComplexity.polForm, with the last guess required to accept.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.akLadderF start k 0 x x_1 none = ⊥
• DescriptiveComplexity.akLadderF start k 0 x x_1 (some j) = DescriptiveComplexity.akAccClause j

noncomputable def DescriptiveComplexity.akKernel (start : Bool) (k : ℕ) : (akLang k).Sentence

The kernel of the Σₖ sentence: the instance is a well-formed alternating machine with a start state, and the ladder holds of the guessed rounds.

Equations

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

theorem DescriptiveComplexity.realize_akKernel {k : ℕ} {A : Type} [instA : (FirstOrder.Language.turingAlt k).Structure A] (ρs : Fin k → tmGuessBlock.Assignment A) (start : Bool) : A ⊨ akKernel start k ↔ (atmData k A).WellFormed ∧ (atmData k A).BlocksWellFormed k ∧ (∃ (q : A), (atmData k A).Start q) ∧ (atmData k A).runMatrix start k 0 none ρs