Peeling the blocks of the prefix

The prefix of the constructed instance is read block by block: the two endpoints (DescriptiveComplexity.tEnds), then for each level in increasing order its midpoint (DescriptiveComplexity.tZ), its universal bit (DescriptiveComplexity.tB) and the pair it passes below (DescriptiveComplexity.tUV), and finally the auxiliary variables (DescriptiveComplexity.tAux).

The whole of that reading is the five transition lemmas below (DescriptiveComplexity.step_ends, DescriptiveComplexity.step_z, DescriptiveComplexity.step_b, DescriptiveComplexity.step_uv, DescriptiveComplexity.step_last), each an instance of DescriptiveComplexity.qPlayed_step: recognizing which block comes next is a computation on block coordinates, and every variable's block coordinates are one of three shapes (DescriptiveComplexity.keyTriple_cases).

theorem DescriptiveComplexity.keyTriple_cases {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : QVarTag} {p q : A} (h : QVarOn v p q) : keyTriple v p q = (0, qBot A, 0) ∨ (∃ (ℓ : A), IsSV ℓ ∧ ∃ s ≤ 2, keyTriple v p q = (1, ℓ, s)) ∨ keyTriple v p q = (2, qBot A, 0)

The block coordinates of a variable are those of the endpoints, of a slot of a level, or of the auxiliary variables.

Comparing block coordinates

theorem DescriptiveComplexity.tripleLt_mk {A : Type} [LinearOrder A] (g s g' s' : ℕ) (a a' : A) : TripleLt (g, a, s) (g', a', s') ↔ g < g' ∨ g = g' ∧ (a < a' ∨ a = a' ∧ s < s')

theorem DescriptiveComplexity.tripleLt_grp {A : Type} [LinearOrder A] {g g' s s' : ℕ} {a a' : A} (h : g < g') : TripleLt (g, a, s) (g', a', s')

theorem DescriptiveComplexity.not_tripleLt_grp {A : Type} [LinearOrder A] {g g' s s' : ℕ} {a a' : A} (h : g' < g) : ¬TripleLt (g, a, s) (g', a', s')

theorem DescriptiveComplexity.triple_ne_grp {A : Type} {g g' s s' : ℕ} {a a' : A} (h : g ≠ g') : (g, a, s) ≠ (g', a', s')

theorem DescriptiveComplexity.tripleLt_lev {A : Type} [LinearOrder A] {ℓ'' ℓ : A} {s k : ℕ} : TripleLt (1, ℓ'', s) (1, ℓ, k) ↔ ℓ'' < ℓ ∨ ℓ'' = ℓ ∧ s < k

theorem DescriptiveComplexity.triple_eq_lev {A : Type} {ℓ'' ℓ : A} {s k : ℕ} : (1, ℓ'', s) = (1, ℓ, k) ↔ ℓ'' = ℓ ∧ s = k

The five transitions

theorem DescriptiveComplexity.qPlayed_tEnds {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : QPlayed (tEnds A) = fun (x : QM A) => False

Before the endpoints nothing has been quantified.

theorem DescriptiveComplexity.step_ends {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {ℓ : A} (hmin : IsMinSV ℓ) : qUnion (QPlayed (tEnds A)) (QBlk (tEnds A)) = QPlayed (tZ ℓ)

After the endpoints comes the midpoint of the first level.

theorem DescriptiveComplexity.step_z {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ℓ : A) : qUnion (QPlayed (tZ ℓ)) (QBlk (tZ ℓ)) = QPlayed (tB ℓ)

After the midpoint of a level comes its universal bit.

theorem DescriptiveComplexity.step_b {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (ℓ : A) : qUnion (QPlayed (tB ℓ)) (QBlk (tB ℓ)) = QPlayed (tUV ℓ)

After the universal bit of a level comes the pair it passes below.

theorem DescriptiveComplexity.step_uv {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {ℓ ℓ' : A} (hpred : IsPredSV ℓ ℓ') : qUnion (QPlayed (tUV ℓ)) (QBlk (tUV ℓ)) = QPlayed (tZ ℓ')

After the pair of a level comes the midpoint of the next one.

theorem DescriptiveComplexity.step_last {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {ℓ : A} (hmax : IsMaxSV ℓ) : qUnion (QPlayed (tUV ℓ)) (QBlk (tUV ℓ)) = QPlayed (tAux A)

After the pair of the last level come the auxiliary variables.

theorem DescriptiveComplexity.all_played {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (x : QM A) : IsQVar x → qUnion (QPlayed (tAux A)) (QBlk (tAux A)) x

Once the auxiliary variables are quantified, everything is.

The polarity of each block

theorem DescriptiveComplexity.blk_ex {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {T : ℕ × A × ℕ} (h : ∀ (v : QVarTag) (p q : A), QVarOn v p q → keyTriple v p q = T → v ≠ QVarTag.sB) (x : QM A) : QBlk T x → ¬IsQAll x

theorem DescriptiveComplexity.blk_all {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {T : ℕ × A × ℕ} (h : ∀ (v : QVarTag) (p q : A), QVarOn v p q → keyTriple v p q = T → v = QVarTag.sB) (x : QM A) : QBlk T x → IsQAll x

theorem DescriptiveComplexity.blk_ex_tEnds {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (x : QM A) : QBlk (tEnds A) x → ¬IsQAll x

theorem DescriptiveComplexity.blk_ex_tZ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ℓ : A) (x : QM A) : QBlk (tZ ℓ) x → ¬IsQAll x

theorem DescriptiveComplexity.blk_ex_tUV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ℓ : A) (x : QM A) : QBlk (tUV ℓ) x → ¬IsQAll x

theorem DescriptiveComplexity.blk_ex_tAux {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (x : QM A) : QBlk (tAux A) x → ¬IsQAll x

theorem DescriptiveComplexity.blk_all_tB {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ℓ : A) (x : QM A) : QBlk (tB ℓ) x → IsQAll x