The blocks of the prefix, and what the matrix says

The five kinds of block the prefix of the constructed instance splits into – the endpoints, then a midpoint, a universal bit and a pair per level, then the auxiliary variables (DescriptiveComplexity.tEnds, DescriptiveComplexity.tZ, DescriptiveComplexity.tB, DescriptiveComplexity.tUV, DescriptiveComplexity.tAux) – together with the reading of the matrix they make possible.

Grouping the clause tags by what they talk about turns the matrix into four conditions (DescriptiveComplexity.qsatMatrix_iff_parts): the source valuation witnesses DescriptiveComplexity.IsStart for the first endpoint (DescriptiveComplexity.SrcPart), the target valuation witnesses DescriptiveComplexity.IsGoal for the second (DescriptiveComplexity.TgtPart), the transition valuation and the bit sE witness one move of the walk at the bottom level (DescriptiveComplexity.StepPart), and every level relates its own pair to the pair it receives from above (DescriptiveComplexity.LevPart).

Each group is the conjunction of two clauses of opposite signs, which is why the conditions come out as equivalences rather than implications.

The block coordinates

@[simp]

theorem DescriptiveComplexity.keyTriple_sS {A : Type} (p q : A) : keyTriple QVarTag.sS p q = (0, q, 0)

@[simp]

theorem DescriptiveComplexity.keyTriple_sT {A : Type} (p q : A) : keyTriple QVarTag.sT p q = (0, q, 0)

@[simp]

theorem DescriptiveComplexity.keyTriple_sZ {A : Type} (p q : A) : keyTriple QVarTag.sZ p q = (1, p, 0)

@[simp]

theorem DescriptiveComplexity.keyTriple_sB {A : Type} (p q : A) : keyTriple QVarTag.sB p q = (1, p, 1)

@[simp]

theorem DescriptiveComplexity.keyTriple_sU {A : Type} (p q : A) : keyTriple QVarTag.sU p q = (1, p, 2)

@[simp]

theorem DescriptiveComplexity.keyTriple_sV {A : Type} (p q : A) : keyTriple QVarTag.sV p q = (1, p, 2)

@[simp]

theorem DescriptiveComplexity.keyTriple_aS {A : Type} (p q : A) : keyTriple QVarTag.aS p q = (2, q, 0)

@[simp]

theorem DescriptiveComplexity.keyTriple_aT {A : Type} (p q : A) : keyTriple QVarTag.aT p q = (2, q, 0)

@[simp]

theorem DescriptiveComplexity.keyTriple_aP {A : Type} (p q : A) : keyTriple QVarTag.aP p q = (2, q, 0)

@[simp]

theorem DescriptiveComplexity.keyTriple_sE {A : Type} (p q : A) : keyTriple QVarTag.sE p q = (2, q, 0)

noncomputable def DescriptiveComplexity.tEnds (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : ℕ × A × ℕ

The block coordinates of the two endpoints of the walk: the first block.

Equations

• DescriptiveComplexity.tEnds A = (0, DescriptiveComplexity.qBot A, 0)

def DescriptiveComplexity.tZ {A : Type} (ℓ : A) : ℕ × A × ℕ

The block coordinates of the midpoint guessed at level ℓ.

Equations

• DescriptiveComplexity.tZ ℓ = (1, ℓ, 0)

def DescriptiveComplexity.tB {A : Type} (ℓ : A) : ℕ × A × ℕ

The block coordinates of the universal bit of level ℓ.

Equations

• DescriptiveComplexity.tB ℓ = (1, ℓ, 1)

def DescriptiveComplexity.tUV {A : Type} (ℓ : A) : ℕ × A × ℕ

The block coordinates of the pair passed below level ℓ.

Equations

• DescriptiveComplexity.tUV ℓ = (1, ℓ, 2)

noncomputable def DescriptiveComplexity.tAux (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : ℕ × A × ℕ

The block coordinates of the auxiliary variables: the last block.

Equations

• DescriptiveComplexity.tAux A = (2, DescriptiveComplexity.qBot A, 0)

Overriding a block

theorem DescriptiveComplexity.qOver_out {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {B : QM A → Prop} (τ ν : QM A → Prop) {v : QVarTag} {p q : A} (h : ¬B (qVar v p q)) : qOver B τ ν (qVar v p q) ↔ τ (qVar v p q)

theorem DescriptiveComplexity.qOver_in {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {B : QM A → Prop} (τ ν : QM A → Prop) {v : QVarTag} {p q : A} (h : B (qVar v p q)) : qOver B τ ν (qVar v p q) ↔ ν (qVar v p q)

Two clauses of opposite signs make an equivalence

theorem DescriptiveComplexity.iff_of_or_not {P Q : Prop} (h0 : ¬P ∨ Q) (h1 : P ∨ ¬Q) : P ↔ Q

theorem DescriptiveComplexity.or_forall_of_forall_or {ι : Sort u_1} {R : Prop} {P : ι → Prop} (h : ∀ (i : ι), R ∨ P i) : R ∨ ∀ (i : ι), P i

What the matrix says

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

The source valuation satisfies the source clauses and reads the source endpoint of the walk.

Equations

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

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

The target valuation satisfies the target clauses and reads the target endpoint of the walk.

Equations

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

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

The base case of the recursion: either the equality branch, or the transition valuation satisfying the transition clauses while reading the first component of the bottom pair and writing the second.

Equations

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

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

Every level relates its pair to the pair it receives from above.

Equations

• DescriptiveComplexity.LevPart σ = ∀ (b w s : Bool) (ℓ x : A), DescriptiveComplexity.IsSV ℓ → DescriptiveComplexity.IsSV x → DescriptiveComplexity.LevSat σ b w s ℓ x

theorem DescriptiveComplexity.matrix_cSrc_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) : (∀ (p q : A), QClOn QClTag.cSrc p q → ClSat σ QClTag.cSrc p q) ↔ ClausesHold A (valS σ) FirstOrder.Language.tsSrcCl

theorem DescriptiveComplexity.matrix_cTgt_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) : (∀ (p q : A), QClOn QClTag.cTgt p q → ClSat σ QClTag.cTgt p q) ↔ ClausesHold A (valT σ) FirstOrder.Language.tsTgtCl

theorem DescriptiveComplexity.matrix_cStep_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) : (∀ (p q : A), QClOn QClTag.cStep p q → ClSat σ QClTag.cStep p q) ↔ bitE σ ∨ ClausesHold A (valP σ) FirstOrder.Language.tsStepCl

theorem DescriptiveComplexity.matrix_lS_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) : (∀ (s : Bool) (p q : A), QClOn (QClTag.lS s) p q → ClSat σ (QClTag.lS s) p q) ↔ ReadsCur A (valS σ) (stS σ)

theorem DescriptiveComplexity.matrix_lT_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) : (∀ (s : Bool) (p q : A), QClOn (QClTag.lT s) p q → ClSat σ (QClTag.lT s) p q) ↔ ReadsCur A (valT σ) (stT σ)

theorem DescriptiveComplexity.matrix_lU_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) : (∀ (s : Bool) (p q : A), QClOn (QClTag.lU s) p q → ClSat σ (QClTag.lU s) p q) ↔ ∀ (m : A), IsMaxSV m → bitE σ ∨ ReadsCur A (valP σ) (stU σ m)

theorem DescriptiveComplexity.matrix_lV_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) : (∀ (s : Bool) (p q : A), QClOn (QClTag.lV s) p q → ClSat σ (QClTag.lV s) p q) ↔ ∀ (m : A), IsMaxSV m → bitE σ ∨ WritesNext A (valP σ) (stV σ m)

theorem DescriptiveComplexity.matrix_bE_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) : (∀ (s : Bool) (p q : A), QClOn (QClTag.bE s) p q → ClSat σ (QClTag.bE s) p q) ↔ ∀ (m : A), IsMaxSV m → ¬bitE σ ∨ ∀ (x : A), IsSV x → (stU σ m x ↔ stV σ m x)

theorem DescriptiveComplexity.matrix_lev_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) : (∀ (b w s : Bool) (ℓ x : A), QClOn (QClTag.lev b w s) ℓ x → ClSat σ (QClTag.lev b w s) ℓ x) ↔ LevPart σ

theorem DescriptiveComplexity.qsatMatrix_iff_parts {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) : QsatMatrix σ ↔ SrcPart σ ∧ TgtPart σ ∧ StepPart σ ∧ LevPart σ

The matrix, read semantically.