The innermost block: the base case of the recursion

The last block of the prefix quantifies the three auxiliary valuations and the bit sE, and is immediately followed by the matrix. Peeling it (DescriptiveComplexity.game_aux) turns the position it opens into exactly three independent conditions – the source endpoint is a start state, the target endpoint is a goal state, and the pair passed below the last level is one move of the walk (DescriptiveComplexity.SavStep) – together with the level clauses, which the auxiliary variables do not touch.

The three conditions are independent because the three valuations are read on disjoint sets of elements, which is what lets the single existential quantifier over the block be split (DescriptiveComplexity.auxVal).

Readouts a block does not touch

theorem DescriptiveComplexity.not_qBlk_of_ne {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {T : ℕ × A × ℕ} {v : QVarTag} {p q : A} (h : keyTriple v p q ≠ T) : ¬QBlk T (qVar v p q)

theorem DescriptiveComplexity.readout_out {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {T : ℕ × A × ℕ} {v : QVarTag} {p q : A} (τ ν : QM A → Prop) (h : keyTriple v p q ≠ T) : qOver (QBlk T) τ ν (qVar v p q) ↔ τ (qVar v p q)

theorem DescriptiveComplexity.readout_in {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {T : ℕ × A × ℕ} {v : QVarTag} {p q : A} (τ ν : QM A → Prop) (hv : QVarOn v p q) (h : keyTriple v p q = T) : qOver (QBlk T) τ ν (qVar v p q) ↔ ν (qVar v p q)

@[simp]

theorem DescriptiveComplexity.stS_over_tAux {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ ν : QM A → Prop) : stS (qOver (QBlk (tAux A)) τ ν) = stS τ

@[simp]

theorem DescriptiveComplexity.stT_over_tAux {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ ν : QM A → Prop) : stT (qOver (QBlk (tAux A)) τ ν) = stT τ

@[simp]

theorem DescriptiveComplexity.stU_over_tAux {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ ν : QM A → Prop) (ℓ : A) : stU (qOver (QBlk (tAux A)) τ ν) ℓ = stU τ ℓ

@[simp]

theorem DescriptiveComplexity.stV_over_tAux {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ ν : QM A → Prop) (ℓ : A) : stV (qOver (QBlk (tAux A)) τ ν) ℓ = stV τ ℓ

@[simp]

theorem DescriptiveComplexity.stZ_over_tAux {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ ν : QM A → Prop) (ℓ : A) : stZ (qOver (QBlk (tAux A)) τ ν) ℓ = stZ τ ℓ

@[simp]

theorem DescriptiveComplexity.bitB_over_tAux {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ ν : QM A → Prop) (ℓ : A) : bitB (qOver (QBlk (tAux A)) τ ν) ℓ ↔ bitB τ ℓ

theorem DescriptiveComplexity.levSat_over_tAux {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ ν : QM A → Prop) (b w s : Bool) (ℓ x : A) : LevSat (qOver (QBlk (tAux A)) τ ν) b w s ℓ x ↔ LevSat τ b w s ℓ x

Splitting the last existential quantifier

def DescriptiveComplexity.auxVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (f g h : A → Prop) (e : Prop) : QM A → Prop

The assignment of the last block made of three valuations and a bit.

Equations

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

@[simp]

theorem DescriptiveComplexity.valS_over_tAux {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ : QM A → Prop) (f g h : A → Prop) (e : Prop) : valS (qOver (QBlk (tAux A)) τ (auxVal f g h e)) = f

@[simp]

theorem DescriptiveComplexity.valT_over_tAux {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ : QM A → Prop) (f g h : A → Prop) (e : Prop) : valT (qOver (QBlk (tAux A)) τ (auxVal f g h e)) = g

@[simp]

theorem DescriptiveComplexity.valP_over_tAux {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ : QM A → Prop) (f g h : A → Prop) (e : Prop) : valP (qOver (QBlk (tAux A)) τ (auxVal f g h e)) = h

@[simp]

theorem DescriptiveComplexity.bitE_over_tAux {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ : QM A → Prop) (f g h : A → Prop) (e : Prop) : bitE (qOver (QBlk (tAux A)) τ (auxVal f g h e)) ↔ e

The base case

theorem DescriptiveComplexity.game_aux {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ : QM A → Prop) : QsatWins (QPlayed (tAux A)) τ ↔ IsStart A (stS τ) ∧ IsGoal A (stT τ) ∧ LevPart τ ∧ ∀ (m : A), IsMaxSV m → SavStep stCls (StepRel A) (stU τ m) (stV τ m)

The innermost block, played: the auxiliary valuations witness that the source endpoint is a start state, that the target endpoint is a goal state, and that the pair passed below the last level is one move of the walk; the level clauses do not mention them.