The levels of the Savitch recursion, and what a valuation reads

Two independent pieces of bookkeeping for the correctness proof.

Levels

Levels are the state variables of the input, in the ambient order: the first one (DescriptiveComplexity.IsMinSV) carries the two endpoints of the walk, the last one (DescriptiveComplexity.IsMaxSV) the base case, and each other level receives its pair from the level just above (DescriptiveComplexity.IsPredSV). Those three notions exist and are unique on a finite order, and DescriptiveComplexity.svAbove – the number of levels from a given one down to the last – decreases by one at each step, starting from DescriptiveComplexity.stateDepth at the first level and ending at 1. That is the depth of DescriptiveComplexity.SavPow the level computes.

What a valuation reads

A valuation of the constructed instance is a predicate on its elements; the correctness proof only ever reads it through the ten projections below (DescriptiveComplexity.stS, DescriptiveComplexity.stU, DescriptiveComplexity.bitB, DescriptiveComplexity.valP…), one per variable tag, which turn it back into the states, bits and valuations the reduction means.

The minimum of the input order

noncomputable def DescriptiveComplexity.qBot (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : A

The minimum of the input order: the padding of the coordinates a tag does not use.

Equations

• DescriptiveComplexity.qBot A = ⋯.choose

theorem DescriptiveComplexity.isBot_qBot (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : IsBot (qBot A)

theorem DescriptiveComplexity.eq_qBot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {q : A} (h : IsBot q) : q = qBot A

@[simp]

theorem DescriptiveComplexity.isBot_iff_eq_qBot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {q : A} : IsBot q ↔ q = qBot A

The levels

theorem DescriptiveComplexity.IsMinSV.isSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {ℓ : A} (h : IsMinSV ℓ) : IsSV ℓ

theorem DescriptiveComplexity.IsMaxSV.isSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {ℓ : A} (h : IsMaxSV ℓ) : IsSV ℓ

theorem DescriptiveComplexity.IsMinSV.le {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {ℓ z : A} (h : IsMinSV ℓ) (hz : IsSV z) : ℓ ≤ z

theorem DescriptiveComplexity.IsMaxSV.le {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {ℓ z : A} (h : IsMaxSV ℓ) (hz : IsSV z) : z ≤ ℓ

theorem DescriptiveComplexity.isMinSV_unique {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {ℓ ℓ' : A} (h : IsMinSV ℓ) (h' : IsMinSV ℓ') : ℓ = ℓ'

theorem DescriptiveComplexity.isMaxSV_unique {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {ℓ ℓ' : A} (h : IsMaxSV ℓ) (h' : IsMaxSV ℓ') : ℓ = ℓ'

theorem DescriptiveComplexity.isPredSV_unique {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {d d' ℓ : A} (h : IsPredSV d ℓ) (h' : IsPredSV d' ℓ) : d = d'

theorem DescriptiveComplexity.exists_isMinSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] {x : A} (hx : IsSV x) : ∃ (ℓ : A), IsMinSV ℓ

theorem DescriptiveComplexity.exists_isMaxSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] {x : A} (hx : IsSV x) : ∃ (ℓ : A), IsMaxSV ℓ

theorem DescriptiveComplexity.exists_isPredSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] {ℓ : A} (hℓ : IsSV ℓ) (hmin : ¬IsMinSV ℓ) : ∃ (d : A), IsPredSV d ℓ

theorem DescriptiveComplexity.IsPredSV.not_isMinSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {d ℓ : A} (h : IsPredSV d ℓ) : ¬IsMinSV ℓ

noncomputable def DescriptiveComplexity.svAbove {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (ℓ : A) : ℕ

The number of levels from ℓ down to the last one: the depth of the Savitch recursion that level ℓ still has to unfold.

Equations

• DescriptiveComplexity.svAbove ℓ = {z : A | DescriptiveComplexity.IsSV z ∧ ℓ ≤ z}.ncard

theorem DescriptiveComplexity.svAbove_of_isMaxSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {ℓ : A} (h : IsMaxSV ℓ) : svAbove ℓ = 1

theorem DescriptiveComplexity.svAbove_of_isPredSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] {d ℓ : A} (h : IsPredSV d ℓ) : svAbove d = svAbove ℓ + 1

theorem DescriptiveComplexity.svAbove_of_isMinSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {ℓ : A} (h : IsMinSV ℓ) : svAbove ℓ = stateDepth A

theorem DescriptiveComplexity.exists_isSuccSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] {ℓ : A} (hℓ : IsSV ℓ) (hmax : ¬IsMaxSV ℓ) : ∃ (ℓ' : A), IsPredSV ℓ ℓ'

theorem DescriptiveComplexity.svAbove_pos {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] {ℓ : A} (hℓ : IsSV ℓ) : 0 < svAbove ℓ

What a valuation reads

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

The source endpoint of the walk, as read by a valuation.

Equations

• DescriptiveComplexity.stS σ a = σ (DescriptiveComplexity.qVar DescriptiveComplexity.QVarTag.sS a (DescriptiveComplexity.qBot A))

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

The target endpoint of the walk, as read by a valuation.

Equations

• DescriptiveComplexity.stT σ a = σ (DescriptiveComplexity.qVar DescriptiveComplexity.QVarTag.sT a (DescriptiveComplexity.qBot A))

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

The midpoint guessed at a level, as read by a valuation.

Equations

• DescriptiveComplexity.stZ σ ℓ a = σ (DescriptiveComplexity.qVar DescriptiveComplexity.QVarTag.sZ ℓ a)

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

The first component of the pair passed below a level.

Equations

• DescriptiveComplexity.stU σ ℓ a = σ (DescriptiveComplexity.qVar DescriptiveComplexity.QVarTag.sU ℓ a)

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

The second component of the pair passed below a level.

Equations

• DescriptiveComplexity.stV σ ℓ a = σ (DescriptiveComplexity.qVar DescriptiveComplexity.QVarTag.sV ℓ a)

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

The universal bit of a level.

Equations

• DescriptiveComplexity.bitB σ ℓ = σ (DescriptiveComplexity.qVar DescriptiveComplexity.QVarTag.sB ℓ (DescriptiveComplexity.qBot A))

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

The valuation satisfying the source clauses.

Equations

• DescriptiveComplexity.valS σ a = σ (DescriptiveComplexity.qVar DescriptiveComplexity.QVarTag.aS a (DescriptiveComplexity.qBot A))

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

The valuation satisfying the target clauses.

Equations

• DescriptiveComplexity.valT σ a = σ (DescriptiveComplexity.qVar DescriptiveComplexity.QVarTag.aT a (DescriptiveComplexity.qBot A))

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

The valuation satisfying the transition clauses.

Equations

• DescriptiveComplexity.valP σ a = σ (DescriptiveComplexity.qVar DescriptiveComplexity.QVarTag.aP a (DescriptiveComplexity.qBot A))

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

The bit saying that the base case is an equality rather than a step.

Equations

• DescriptiveComplexity.bitE σ = σ (DescriptiveComplexity.qVar DescriptiveComplexity.QVarTag.sE (DescriptiveComplexity.qBot A) (DescriptiveComplexity.qBot A))