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 τ ℓ'

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

@[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.bVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ℓ : A) (β : Prop) : QM A → Prop

The assignment of a universal-bit block.

Equations

• DescriptiveComplexity.bVal ℓ β y = (y = DescriptiveComplexity.qVar DescriptiveComplexity.QVarTag.sB ℓ (DescriptiveComplexity.qBot 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.bitB_over_bVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ : QM A → Prop) {ℓ : A} (hℓ : IsSV ℓ) (β : Prop) : bitB (qOver (QBlk (tB ℓ)) τ (bVal ℓ β)) ℓ ↔ β

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 τ

theorem DescriptiveComplexity.inFst_of_isMinSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {ℓ : A} (h : IsMinSV ℓ) (τ : QM A → Prop) : inFst ℓ τ = stS τ

theorem DescriptiveComplexity.inSnd_of_isMinSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {ℓ : A} (h : IsMinSV ℓ) (τ : QM A → Prop) : inSnd ℓ τ = stT τ

theorem DescriptiveComplexity.inFst_of_isPredSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {d ℓ : A} (h : IsPredSV d ℓ) (τ : QM A → Prop) : inFst ℓ τ = stU τ d

theorem DescriptiveComplexity.inSnd_of_isPredSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {d ℓ : A} (h : IsPredSV d ℓ) (τ : QM A → Prop) : inSnd ℓ τ = stV τ d

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

theorem DescriptiveComplexity.levUpto_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {ℓ : A} (hℓ : IsSV ℓ) (τ : QM A → Prop) : LevUpto ℓ τ ↔ LevBelow ℓ τ ∧ ∀ (b w s : Bool) (x : A), IsSV x → LevSat τ b w s ℓ x

theorem DescriptiveComplexity.levIn_fst_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {ℓ : A} (hℓ : IsSV ℓ) (x : A) (s : Bool) : (IsMinSV ℓ ∧ (stS σ x ↔ s = true) ∨ ∃ (d : A), IsPredSV d ℓ ∧ (stU σ d x ↔ s = true)) ↔ (inFst ℓ σ x ↔ s = true)

The input value a level clause compares its own component to.

theorem DescriptiveComplexity.levIn_snd_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {ℓ : A} (hℓ : IsSV ℓ) (x : A) (s : Bool) : (IsMinSV ℓ ∧ (stT σ x ↔ s = true) ∨ ∃ (d : A), IsPredSV d ℓ ∧ (stV σ d x ↔ s = true)) ↔ (inSnd ℓ σ x ↔ s = true)

theorem DescriptiveComplexity.levSat_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {ℓ : A} (hℓ : IsSV ℓ) (b w s : Bool) (x : A) : LevSat σ b w s ℓ x ↔ (bitB σ ℓ ↔ (!b) = true) ∨ ((if w = true then stV σ ℓ x else stU σ ℓ x) ↔ (!s) = true) ∨ ((if b = w then stZ σ ℓ x else if b = true then inFst ℓ σ x else inSnd ℓ σ x) ↔ s = true)

A level clause, spelled out: the polarity of the universal bit, the component of the pair it constrains, and the value that component must copy.

theorem DescriptiveComplexity.levSat_tff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {ℓ : A} (hℓ : IsSV ℓ) (x : A) : LevSat σ true false false ℓ x ↔ ¬bitB σ ℓ ∨ stU σ ℓ x ∨ ¬inFst ℓ σ x

theorem DescriptiveComplexity.levSat_tft {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {ℓ : A} (hℓ : IsSV ℓ) (x : A) : LevSat σ true false true ℓ x ↔ ¬bitB σ ℓ ∨ ¬stU σ ℓ x ∨ inFst ℓ σ x

theorem DescriptiveComplexity.levSat_ttf {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {ℓ : A} (hℓ : IsSV ℓ) (x : A) : LevSat σ true true false ℓ x ↔ ¬bitB σ ℓ ∨ stV σ ℓ x ∨ ¬stZ σ ℓ x

theorem DescriptiveComplexity.levSat_ttt {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {ℓ : A} (hℓ : IsSV ℓ) (x : A) : LevSat σ true true true ℓ x ↔ ¬bitB σ ℓ ∨ ¬stV σ ℓ x ∨ stZ σ ℓ x

theorem DescriptiveComplexity.levSat_fff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {ℓ : A} (hℓ : IsSV ℓ) (x : A) : LevSat σ false false false ℓ x ↔ bitB σ ℓ ∨ stU σ ℓ x ∨ ¬stZ σ ℓ x

theorem DescriptiveComplexity.levSat_fft {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {ℓ : A} (hℓ : IsSV ℓ) (x : A) : LevSat σ false false true ℓ x ↔ bitB σ ℓ ∨ ¬stU σ ℓ x ∨ stZ σ ℓ x

theorem DescriptiveComplexity.levSat_ftf {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {ℓ : A} (hℓ : IsSV ℓ) (x : A) : LevSat σ false true false ℓ x ↔ bitB σ ℓ ∨ stV σ ℓ x ∨ ¬inSnd ℓ σ x

theorem DescriptiveComplexity.levSat_ftt {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {ℓ : A} (hℓ : IsSV ℓ) (x : A) : LevSat σ false true true ℓ x ↔ bitB σ ℓ ∨ ¬stV σ ℓ x ∨ inSnd ℓ σ x

theorem DescriptiveComplexity.levSat_all_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {ℓ : A} (hℓ : IsSV ℓ) : (∀ (b w s : Bool) (x : A), IsSV x → LevSat σ b w s ℓ x) ↔ (bitB σ ℓ → ∀ (x : A), IsSV x → (stU σ ℓ x ↔ inFst ℓ σ x) ∧ (stV σ ℓ x ↔ stZ σ ℓ x)) ∧ (¬bitB σ ℓ → ∀ (x : A), IsSV x → (stU σ ℓ x ↔ stZ σ ℓ x) ∧ (stV σ ℓ x ↔ inSnd ℓ σ x))

What the eight clauses of a level say: the pair passed below is the first half of the level when its universal bit holds, the second half otherwise.

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.

theorem DescriptiveComplexity.levSat_congr {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ σ' : QM A → Prop} {ℓ'' : A} (hs : stS σ = stS σ') (ht : stT σ = stT σ') (hz : stZ σ ℓ'' = stZ σ' ℓ'') (hb : bitB σ ℓ'' ↔ bitB σ' ℓ'') (hu : stU σ ℓ'' = stU σ' ℓ'') (hv : stV σ ℓ'' = stV σ' ℓ'') (hup : ∀ (d : A), IsPredSV d ℓ'' → stU σ d = stU σ' d) (hvp : ∀ (d : A), IsPredSV d ℓ'' → stV σ d = stV σ' d) (b w s : Bool) (x : A) : LevSat σ b w s ℓ'' x ↔ LevSat σ' b w s ℓ'' x

@[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.bitB_levOver_ne {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ℓ : A) (τ νZ νB νUV : QM A → Prop) {ℓ'' : A} (h : ℓ'' ≠ ℓ) : bitB (levOver ℓ τ νZ νB νUV) ℓ'' ↔ bitB τ ℓ''

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

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

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

The three blocks of a level leave the levels above it alone.

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.bitB_levOver_bVal {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {ℓ : A} (hℓ : IsSV ℓ) (τ νZ νUV : QM A → Prop) (β : Prop) : bitB (levOver ℓ τ νZ (bVal ℓ β) ν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.levPart_iff_levUpto {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {ℓ : A} (hmax : IsMaxSV ℓ) : LevPart σ ↔ LevUpto ℓ σ

theorem DescriptiveComplexity.levBelow_iff_levUpto {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {ℓ ℓ' : A} (hpred : IsPredSV ℓ ℓ') : LevBelow ℓ' σ ↔ LevUpto ℓ σ

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.