One level of the recursion

Playing the three blocks of a level – its midpoint, its universal bit, its pair – is one step of Savitch's recursion (DescriptiveComplexity.game_step): the midpoint is the existentially chosen intermediate state, the universal bit chooses which of the two halves is checked, and the level clauses force the pair passed below to be the endpoints of that half. So the position opened by a level computes DescriptiveComplexity.SavPow at one more than the depth its successor computes.

Iterating that step down the levels and finishing with DescriptiveComplexity.game_aux gives DescriptiveComplexity.game_level: the position opened by a level computes reachability in at most 2 ^ k moves, k the number of levels from it to the last one.

Readouts the three blocks of a level do not touch

@[simp]

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

@[simp]

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

@[simp]

theorem DescriptiveComplexity.stU_over_tZ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (τ ν : QM A → Prop) (ℓ ℓ' : A) : stU (qOver (QBlk (tZ ℓ)) τ ν) ℓ' = stU τ ℓ'

@[simp]

theorem DescriptiveComplexity.stV_over_tZ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (τ ν : QM A → Prop) (ℓ ℓ' : A) : stV (qOver (QBlk (tZ ℓ)) τ ν) ℓ' = stV τ ℓ'

@[simp]

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

theorem DescriptiveComplexity.stZ_over_tZ_ne {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (τ ν : QM A → Prop) {ℓ ℓ' : A} (h : ℓ' ≠ ℓ) : stZ (qOver (QBlk (tZ ℓ)) τ ν) ℓ' = stZ τ ℓ'

@[simp]

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

@[simp]

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

@[simp]

theorem DescriptiveComplexity.stU_over_tB {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (τ ν : QM A → Prop) (ℓ ℓ' : A) : stU (qOver (QBlk (tB ℓ)) τ ν) ℓ' = stU τ ℓ'

@[simp]

theorem DescriptiveComplexity.stV_over_tB {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (τ ν : QM A → Prop) (ℓ ℓ' : A) : stV (qOver (QBlk (tB ℓ)) τ ν) ℓ' = stV τ ℓ'

@[simp]

theorem DescriptiveComplexity.stZ_over_tB {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (τ ν : QM A → Prop) (ℓ ℓ' : A) : stZ (qOver (QBlk (tB ℓ)) τ ν) ℓ' = stZ τ ℓ'

@[simp]

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

@[simp]

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

@[simp]

theorem DescriptiveComplexity.stZ_over_tUV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (τ ν : QM A → Prop) (ℓ ℓ' : A) : stZ (qOver (QBlk (tUV ℓ)) τ ν) ℓ' = stZ τ ℓ'

@[simp]

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

theorem DescriptiveComplexity.stU_over_tUV_ne {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (τ ν : QM A → Prop) {ℓ ℓ' : A} (h : ℓ' ≠ ℓ) : stU (qOver (QBlk (tUV ℓ)) τ ν) ℓ' = stU τ ℓ'

theorem DescriptiveComplexity.stV_over_tUV_ne {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (τ ν : QM A → Prop) {ℓ ℓ' : A} (h : ℓ' ≠ ℓ) : stV (qOver (QBlk (tUV ℓ)) τ ν) ℓ' = stV τ ℓ'

Assignments of the three blocks of a level

def DescriptiveComplexity.zVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ℓ : A) (Z : A → Prop) : QM A → Prop

The assignment of a midpoint block.

Equations

• DescriptiveComplexity.zVal ℓ Z y = ∃ (a : A), y = DescriptiveComplexity.qVar DescriptiveComplexity.QVarTag.sZ ℓ a ∧ Z a

def DescriptiveComplexity.uvVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ℓ : A) (U V : A → Prop) : QM A → Prop

The assignment of a pair block.

Equations

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

theorem DescriptiveComplexity.stZ_over_zVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (τ : QM A → Prop) {ℓ : A} (hℓ : IsSV ℓ) (Z : A → Prop) {a : A} (ha : IsSV a) : stZ (qOver (QBlk (tZ ℓ)) τ (zVal ℓ Z)) ℓ a ↔ Z a

theorem DescriptiveComplexity.stU_over_uvVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (τ : QM A → Prop) {ℓ : A} (hℓ : IsSV ℓ) (U V : A → Prop) {a : A} (ha : IsSV a) : stU (qOver (QBlk (tUV ℓ)) τ (uvVal ℓ U V)) ℓ a ↔ U a

theorem DescriptiveComplexity.stV_over_uvVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (τ : QM A → Prop) {ℓ : A} (hℓ : IsSV ℓ) (U V : A → Prop) {a : A} (ha : IsSV a) : stV (qOver (QBlk (tUV ℓ)) τ (uvVal ℓ U V)) ℓ a ↔ V a

The pair a level receives, and the clauses of the levels above

noncomputable def DescriptiveComplexity.inFst {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ℓ : A) (τ : QM A → Prop) : A → Prop

The first component of the pair a level receives: the source endpoint at the first level, the first component of the level above otherwise.

Equations

• DescriptiveComplexity.inFst ℓ τ = if h : ∃ (d : A), DescriptiveComplexity.IsPredSV d ℓ then DescriptiveComplexity.stU τ h.choose else DescriptiveComplexity.stS τ

noncomputable def DescriptiveComplexity.inSnd {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ℓ : A) (τ : QM A → Prop) : A → Prop

The second component of the pair a level receives.

Equations

• DescriptiveComplexity.inSnd ℓ τ = if h : ∃ (d : A), DescriptiveComplexity.IsPredSV d ℓ then DescriptiveComplexity.stV τ h.choose else DescriptiveComplexity.stT τ

def DescriptiveComplexity.LevBelow {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ℓ : A) (τ : QM A → Prop) : Prop

The clauses of every level strictly above ℓ hold.

Equations

• DescriptiveComplexity.LevBelow ℓ τ = ∀ (b w s : Bool) (ℓ'' x : A), DescriptiveComplexity.IsSV ℓ'' → ℓ'' < ℓ → DescriptiveComplexity.IsSV x → DescriptiveComplexity.LevSat τ b w s ℓ'' x

def DescriptiveComplexity.LevUpto {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ℓ : A) (τ : QM A → Prop) : Prop

The clauses of every level down to ℓ hold.

Equations

• DescriptiveComplexity.LevUpto ℓ τ = ∀ (b w s : Bool) (ℓ'' x : A), DescriptiveComplexity.IsSV ℓ'' → ℓ'' ≤ ℓ → DescriptiveComplexity.IsSV x → DescriptiveComplexity.LevSat τ b w s ℓ'' x

The three blocks of a level leave the other levels alone

def DescriptiveComplexity.levOver {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ℓ : A) (τ νZ νB νUV : QM A → Prop) : QM A → Prop

The abbreviation for the valuation obtained by playing the three blocks of level ℓ.

Equations

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

@[simp]

theorem DescriptiveComplexity.stS_levOver {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ℓ : A) (τ νZ νB νUV : QM A → Prop) : stS (levOver ℓ τ νZ νB νUV) = stS τ

@[simp]

theorem DescriptiveComplexity.stT_levOver {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ℓ : A) (τ νZ νB νUV : QM A → Prop) : stT (levOver ℓ τ νZ νB νUV) = stT τ

@[simp]

theorem DescriptiveComplexity.stZ_levOver {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ℓ : A) (τ νZ νB νUV : QM A → Prop) (ℓ'' : A) : stZ (levOver ℓ τ νZ νB νUV) ℓ'' = stZ (qOver (QBlk (tZ ℓ)) τ νZ) ℓ''

theorem DescriptiveComplexity.stU_levOver_ne {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ℓ : A) (τ νZ νB νUV : QM A → Prop) {ℓ'' : A} (h : ℓ'' ≠ ℓ) : stU (levOver ℓ τ νZ νB νUV) ℓ'' = stU τ ℓ''

theorem DescriptiveComplexity.stV_levOver_ne {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ℓ : A) (τ νZ νB νUV : QM A → Prop) {ℓ'' : A} (h : ℓ'' ≠ ℓ) : stV (levOver ℓ τ νZ νB νUV) ℓ'' = stV τ ℓ''

theorem DescriptiveComplexity.levOver_eq {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ℓ : A) (τ νZ νB νUV : QM A → Prop) : qOver (QBlk (tUV ℓ)) (qOver (QBlk (tB ℓ)) (qOver (QBlk (tZ ℓ)) τ νZ) νB) νUV = levOver ℓ τ νZ νB νUV

theorem DescriptiveComplexity.stU_levOver_uvVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {ℓ : A} (hℓ : IsSV ℓ) (τ νZ νB : QM A → Prop) (U V : A → Prop) {a : A} (ha : IsSV a) : stU (levOver ℓ τ νZ νB (uvVal ℓ U V)) ℓ a ↔ U a

theorem DescriptiveComplexity.stV_levOver_uvVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {ℓ : A} (hℓ : IsSV ℓ) (τ νZ νB : QM A → Prop) (U V : A → Prop) {a : A} (ha : IsSV a) : stV (levOver ℓ τ νZ νB (uvVal ℓ U V)) ℓ a ↔ V a

theorem DescriptiveComplexity.stZ_levOver_zVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {ℓ : A} (hℓ : IsSV ℓ) (τ : QM A → Prop) (Z : A → Prop) {a : A} (ha : IsSV a) : stZ (qOver (QBlk (tZ ℓ)) τ (zVal ℓ Z)) ℓ a ↔ Z a

One level of the recursion

theorem DescriptiveComplexity.game_step {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {ℓ : A} (hℓ : IsSV ℓ) {k : ℕ} {nxt : ℕ × A × ℕ} (hnxt : qUnion (QPlayed (tUV ℓ)) (QBlk (tUV ℓ)) = QPlayed nxt) (IH : ∀ (σ : QM A → Prop), QsatWins (QPlayed nxt) σ ↔ IsStart A (stS σ) ∧ IsGoal A (stT σ) ∧ LevUpto ℓ σ ∧ SavPow stCls (StepRel A) k (stU σ ℓ) (stV σ ℓ)) (τ : QM A → Prop) : QsatWins (QPlayed (tZ ℓ)) τ ↔ IsStart A (stS τ) ∧ IsGoal A (stT τ) ∧ LevBelow ℓ τ ∧ SavPow stCls (StepRel A) (k + 1) (inFst ℓ τ) (inSnd ℓ τ)

Playing the three blocks of a level is one step of Savitch's recursion. The midpoint is the intermediate state, the universal bit chooses which half is checked, and the level clauses force the pair passed below to be the endpoints of that half.

Down the levels

theorem DescriptiveComplexity.game_level {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (n : ℕ) (ℓ : A) : IsSV ℓ → svAbove ℓ ≤ n → ∀ (τ : QM A → Prop), QsatWins (QPlayed (tZ ℓ)) τ ↔ IsStart A (stS τ) ∧ IsGoal A (stT τ) ∧ LevBelow ℓ τ ∧ SavPow stCls (StepRel A) (svAbove ℓ) (inFst ℓ τ) (inSnd ℓ τ)

The position opened by a level computes reachability in at most 2 ^ k moves, k the number of levels from it down to the last one.