≡ᵏ-invariance of the fixed-point stages

The stages of a simultaneous first-order induction cannot separate ≡ᵏ-equivalent tuples, when k covers the induction's variable budget (DescriptiveComplexity.StepDef.VarBound: each variable's arity plus the quantifier depth of its step formula) and the equivalence is taken relative to a family of relation symbols covering those of the induction (DescriptiveComplexity.StepDef.UsesRels; every induction has a finite such family, DescriptiveComplexity.StepDef.exists_usesRels). This is the reason the unordered Abiteboul–Vianu theorem is about P = PSPACE rather than a triviality: an inflationary or partial induction over a bare structure only ever computes ≡ᵏ-invariant relations, so everything it derives factors through the ≡ᵏ-classes.

The induction is one step of bookkeeping on top of the k-variable invariance lemma (DescriptiveComplexity.realize_formula_equivK): the previous stage is invariant by induction hypothesis, so expanding the structure by it does not change ≡ᵏ (DescriptiveComplexity.equivK_structure₁_eq, the expansion lemma DescriptiveComplexity.equivK_inf_eq read at a block expansion – the block's own symbols joining the agreement family through DescriptiveComplexity.blockRelsExtend), so the step formulas – within budget – cannot separate equivalent tuples, so the next stage is invariant (DescriptiveComplexity.StepDef.next_invariant). Neither iteration is special: inflationary and partial stages inherit invariance from next alone (DescriptiveComplexity.StepDef.inflStage_invariant, DescriptiveComplexity.StepDef.partStage_invariant).

Every induction has a budget (DescriptiveComplexity.StepDef.exists_varBound): k and the family are chosen per definition, which is exactly how the invariant layer is consumed – each phase-G statement carries the k and the symbols of the definition it starts from.

Invariant assignments

def DescriptiveComplexity.AssignInvariant {L : FirstOrder.Language} (S : Set ((n : ℕ) × L.Relations n)) (A : Type) [L.Structure A] (k : ℕ) {B : SOBlock} (ρ : B.Assignment A) : Prop

An assignment of a block is ≡ᵏ-invariant (relative to the agreement family S) when each of its relations cannot separate ≡ᵏ-equivalent tuples, however its arguments are selected from the k coordinates.

Equations

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

theorem DescriptiveComplexity.botAssign_invariant {L : FirstOrder.Language} {A : Type} {k : ℕ} {S : Set ((n : ℕ) × L.Relations n)} [L.Structure A] (B : SOBlock) : AssignInvariant S A k (B.botAssign A)

The empty assignment is invariant.

Expanding by an invariant assignment does not change ≡ᵏ

def DescriptiveComplexity.blockRelsExtend {L : FirstOrder.Language} (S : Set ((n : ℕ) × L.Relations n)) (B : SOBlock) : Set ((n : ℕ) × (L.sum B.lang).Relations n)

The agreement family of the block expansion of a structure: the given family on the base symbols, everything on the block symbols.

Equations

• DescriptiveComplexity.blockRelsExtend S B ⟨n, Sum.inl r⟩ = (⟨n, r⟩ ∈ S)
• DescriptiveComplexity.blockRelsExtend S B ⟨fst, Sum.inr val⟩ = True

theorem DescriptiveComplexity.equivK_structure₁_eq {L : FirstOrder.Language} {A : Type} {k : ℕ} {S : Set ((n : ℕ) × L.Relations n)} [L.Structure A] [Finite A] {B : SOBlock} {ρ : B.Assignment A} (hρ : AssignInvariant S A k ρ) : EquivK (atomicAgreeOn (blockRelsExtend S B) A k) = EquivK (atomicAgreeOn S A k)

Expanding the structure by an invariant assignment does not change ≡ᵏ: the expansion lemma DescriptiveComplexity.equivK_inf_eq, read at the block expansion DescriptiveComplexity.SOBlock.structure₁, the block symbols joining the agreement family.

The variable budget and the symbols of an induction

def DescriptiveComplexity.StepDef.VarBound {L : FirstOrder.Language} (d : StepDef L) (k : ℕ) : Prop

The variable budget of a simultaneous induction: k covers each variable's arity together with the quantifier depth of its step formula – enough pebbles to hold the arguments and play out the quantifiers.

Equations

• d.VarBound k = ∀ (i : d.B.ι), d.B.arity i + DescriptiveComplexity.qdepth (d.step i) ≤ k

theorem DescriptiveComplexity.StepDef.exists_varBound {L : FirstOrder.Language} (d : StepDef L) : ∃ (k : ℕ), d.VarBound k

Every induction has a variable budget: the block is finite.

theorem DescriptiveComplexity.StepDef.VarBound.mono {L : FirstOrder.Language} {d : StepDef L} {k k' : ℕ} (h : d.VarBound k) (hkk' : k ≤ k') : d.VarBound k'

A variable budget survives being raised.

def DescriptiveComplexity.StepDef.UsesRels {L : FirstOrder.Language} (d : StepDef L) (S : Set ((n : ℕ) × L.Relations n)) : Prop

The base relation symbols of a simultaneous induction – of its step formulas and its output sentence – lie in the family S.

Equations

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

theorem DescriptiveComplexity.StepDef.UsesRels.mono {L : FirstOrder.Language} {d : StepDef L} {S S' : Set ((n : ℕ) × L.Relations n)} (h : d.UsesRels S) (hSS' : S ⊆ S') : d.UsesRels S'

A family of used symbols survives being enlarged.

theorem DescriptiveComplexity.StepDef.exists_usesRels {L : FirstOrder.Language} (d : StepDef L) : ∃ (S : Set ((n : ℕ) × L.Relations n)), S.Finite ∧ d.UsesRels S

Every induction mentions finitely many base relation symbols: the finite agreement family relative to which its stages are invariant and its refinement is definable.

Invariance of the stages

theorem DescriptiveComplexity.StepDef.next_invariant {L : FirstOrder.Language} {A : Type} {k : ℕ} {S : Set ((n : ℕ) × L.Relations n)} [L.Structure A] [L.IsRelational] [Finite A] (d : StepDef L) (hd : d.VarBound k) (hrels : d.UsesRels S) {ρ : d.B.Assignment A} (hρ : AssignInvariant S A k ρ) : AssignInvariant S A k (d.next ρ)

One application of the step formulas preserves invariance: the k-variable invariance lemma, over the structure expanded by the (invariant) current stage.

theorem DescriptiveComplexity.StepDef.inflStage_invariant {L : FirstOrder.Language} {A : Type} {k : ℕ} {S : Set ((n : ℕ) × L.Relations n)} [L.Structure A] [L.IsRelational] [Finite A] (d : StepDef L) (hd : d.VarBound k) (hrels : d.UsesRels S) (n : ℕ) : AssignInvariant S A k (d.inflStage A n)

Every stage of the inflationary iteration is ≡ᵏ-invariant.

theorem DescriptiveComplexity.StepDef.inflLimit_invariant {L : FirstOrder.Language} {A : Type} {k : ℕ} {S : Set ((n : ℕ) × L.Relations n)} [L.Structure A] [L.IsRelational] [Finite A] (d : StepDef L) (hd : d.VarBound k) (hrels : d.UsesRels S) : AssignInvariant S A k (d.inflLimit A)

The value of the inflationary iteration is ≡ᵏ-invariant: an inflationary induction over a bare structure only computes ≡ᵏ-invariant relations.

theorem DescriptiveComplexity.StepDef.partStage_invariant {L : FirstOrder.Language} {A : Type} {k : ℕ} {S : Set ((n : ℕ) × L.Relations n)} [L.Structure A] [L.IsRelational] [Finite A] (d : StepDef L) (hd : d.VarBound k) (hrels : d.UsesRels S) (n : ℕ) : AssignInvariant S A k (d.partStage A n)

Every stage of the partial iteration is ≡ᵏ-invariant.