Stratified inflationary inductions

Composition of inflationary inductions: a second induction whose step formulas read the converged relations of a first is itself a single induction. The second stratum is presented as a DescriptiveComplexity.StepDef over the base vocabulary expanded by the first stratum's block – its semantics is «run over the structure expanded by the first stratum's limit» – and the composite DescriptiveComplexity.StepDef.stratify computes exactly that value (DescriptiveComplexity.StepDef.ifpHolds_stratify).

The construction gates the second stratum on an arity-0 gate variable, derived once the first stratum's step formulas add nothing to its current stage – a first-order condition, since the step formulas are formulas (DescriptiveComplexity.stratGateF). Inflation makes the timing work: before the gate fires the second stratum is empty; the gate fires exactly when the first stratum has reached its limit, which it then never leaves; from that point on the second stratum replays its own stages verbatim (DescriptiveComplexity.StepDef.strat2Assign_inflStage_add).

Its consumer is the invariant layer of the Abiteboul–Vianu development: the canonical order on ≡ᵏ-classes is one stratum, the simulation of an ordered induction over the invariant structure reads it as a second.

The combined block and its vocabulary

def DescriptiveComplexity.stratBlock (B₁ B₂ : SOBlock) : SOBlock

The block of a stratified induction: the first stratum's variables, an arity-0 gate, the second stratum's variables.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.strat1Sym (L : FirstOrder.Language) (B₁ B₂ : SOBlock) (i : B₁.ι) : (L.sum (stratBlock B₁ B₂).lang).Relations (B₁.arity i)

The relation symbol of a first-stratum variable.

Equations

• DescriptiveComplexity.strat1Sym L B₁ B₂ i = Sum.inr ⟨Sum.inl (Sum.inl i), ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.stratGateSym (L : FirstOrder.Language) (B₁ B₂ : SOBlock) : (L.sum (stratBlock B₁ B₂).lang).Relations 0

The relation symbol of the gate.

Equations

• DescriptiveComplexity.stratGateSym L B₁ B₂ = Sum.inr ⟨Sum.inl (Sum.inr ()), ⋯⟩

def DescriptiveComplexity.strat1Assign {B₁ B₂ : SOBlock} {A : Type} (σ : (stratBlock B₁ B₂).Assignment A) : B₁.Assignment A

The first-stratum part of an assignment of the combined block.

Equations

• DescriptiveComplexity.strat1Assign σ i x = σ (Sum.inl (Sum.inl i)) x

def DescriptiveComplexity.strat2Assign {B₁ B₂ : SOBlock} {A : Type} (σ : (stratBlock B₁ B₂).Assignment A) : B₂.Assignment A

The second-stratum part of an assignment of the combined block.

Equations

• DescriptiveComplexity.strat2Assign σ i x = σ (Sum.inr i) x

def DescriptiveComplexity.StratGate {B₁ B₂ : SOBlock} {A : Type} (σ : (stratBlock B₁ B₂).Assignment A) : Prop

The gate bit of an assignment of the combined block.

Equations

• DescriptiveComplexity.StratGate σ = σ (Sum.inl (Sum.inr ())) Fin.elim0

theorem DescriptiveComplexity.strat1Assign_eq_homAssign {B₁ B₂ : SOBlock} {A : Type} (σ : (stratBlock B₁ B₂).Assignment A) : SOBlock.homAssign (fun (i : B₁.ι) => Sum.inl (Sum.inl i)) ⋯ σ = strat1Assign σ

The first-stratum part is the pullback along the block inclusion.

def DescriptiveComplexity.strat1LHom (L : FirstOrder.Language) (B₁ B₂ : SOBlock) : L.sum B₁.lang →ᴸ L.sum (stratBlock B₁ B₂).lang

The vocabulary morphism reading the first stratum inside the combined block.

Equations

• DescriptiveComplexity.strat1LHom L B₁ B₂ = (FirstOrder.Language.LHom.id L).sumMap (DescriptiveComplexity.SOBlock.homLHom (fun (i : B₁.ι) => Sum.inl (Sum.inl i)) ⋯)

def DescriptiveComplexity.strat2LHom (L : FirstOrder.Language) (B₁ B₂ : SOBlock) : (L.sum B₁.lang).sum B₂.lang →ᴸ L.sum (stratBlock B₁ B₂).lang

The vocabulary morphism reading the doubly expanded vocabulary inside the combined block.

Equations

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

theorem DescriptiveComplexity.realize_strat1Formula {L : FirstOrder.Language} {B₁ B₂ : SOBlock} {A : Type} [L.Structure A] {α : Type} (σ : (stratBlock B₁ B₂).Assignment A) (φ : (L.sum B₁.lang).Formula α) (v : α → A) : ((strat1LHom L B₁ B₂).onFormula φ).Realize v ↔ φ.Realize v

Reading the first stratum inside the combined block: realization against the combined assignment is realization against its first-stratum part.

theorem DescriptiveComplexity.strat2LHom_isExpansionOn {L : FirstOrder.Language} {B₁ B₂ : SOBlock} {A : Type} [L.Structure A] (σ : (stratBlock B₁ B₂).Assignment A) : (strat2LHom L B₁ B₂).IsExpansionOn A

The combined structure is an expansion of the doubly expanded structure along DescriptiveComplexity.strat2LHom.

theorem DescriptiveComplexity.realize_strat2Formula {L : FirstOrder.Language} {B₁ B₂ : SOBlock} {A : Type} [L.Structure A] {α : Type} (σ : (stratBlock B₁ B₂).Assignment A) (φ : ((L.sum B₁.lang).sum B₂.lang).Formula α) (v : α → A) : ((strat2LHom L B₁ B₂).onFormula φ).Realize v ↔ φ.Realize v

Reading the second stratum inside the combined block: realization against the combined assignment is realization over the structure expanded first by the first-stratum part, then by the second.

theorem DescriptiveComplexity.realize_gateAtom {L : FirstOrder.Language} {A : Type} [L.Structure A] {B₁ B₂ : SOBlock} (σ : (stratBlock B₁ B₂).Assignment A) {α : Type} (v : α → A) : ((stratGateSym L B₁ B₂).formula Fin.elim0).Realize v ↔ StratGate σ

Realization of the gate atom: the gate bit of the assignment, whatever the valuation.

The gate formula

noncomputable def DescriptiveComplexity.stratGateF {L : FirstOrder.Language} (d₁ : StepDef L) (B₂ : SOBlock) : (L.sum (stratBlock d₁.B B₂).lang).Formula (Fin 0)

The gate formula: every step formula of the first stratum is absorbed by the current stage – the first stratum has converged.

Equations

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

theorem DescriptiveComplexity.realize_stratGateF {L : FirstOrder.Language} {B₂ : SOBlock} {A : Type} [L.Structure A] (d₁ : StepDef L) (σ : (stratBlock d₁.B B₂).Assignment A) (v : Fin 0 → A) : (stratGateF d₁ B₂).Realize v ↔ ∀ (i : d₁.B.ι) (x : Fin (d₁.B.arity i) → A), d₁.next (strat1Assign σ) i x → strat1Assign σ i x

Realization of the gate formula: the first-stratum part absorbs one more application of the first stratum's steps.

The stratified induction

noncomputable def DescriptiveComplexity.StepDef.stratify {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) : StepDef L

The stratified induction: run the first stratum; once its steps add nothing (the gate), run the second stratum over the frozen first.

Equations

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

theorem DescriptiveComplexity.StepDef.isFixedPt_inflStep_iff {L : FirstOrder.Language} {A : Type} [L.Structure A] (d : StepDef L) (ρ : d.B.Assignment A) : Function.IsFixedPt d.inflStep ρ ↔ ∀ (i : d.B.ι) (x : Fin (d.B.arity i) → A), d.next ρ i x → ρ i x

A step is absorbed by its current stage exactly when the stage is an inflationary fixed point.

theorem DescriptiveComplexity.StepDef.strat1Assign_inflStage {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] (n : ℕ) : strat1Assign ((d₁.stratify d₂).inflStage A n) = d₁.inflStage A n

The first-stratum part of the stratified stages is the first stratum's own stages.

theorem DescriptiveComplexity.StepDef.stratGate_inflStage_succ {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] (n : ℕ) : StratGate ((d₁.stratify d₂).inflStage A (n + 1)) ↔ StratGate ((d₁.stratify d₂).inflStage A n) ∨ Function.IsFixedPt d₁.inflStep (d₁.inflStage A n)

The gate of the stratified stages: false at the start, and derived exactly when the first stratum's current stage is an inflationary fixed point.

theorem DescriptiveComplexity.StepDef.stratGate_mono {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] {m n : ℕ} (hmn : m ≤ n) (h : StratGate ((d₁.stratify d₂).inflStage A m)) : StratGate ((d₁.stratify d₂).inflStage A n)

The gate only ever turns on.

theorem DescriptiveComplexity.StepDef.isFixedPt_of_stratGate {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] {n : ℕ} (h : StratGate ((d₁.stratify d₂).inflStage A n)) : Function.IsFixedPt d₁.inflStep (d₁.inflStage A n)

While the gate is on, the first stratum sits at an inflationary fixed point.

theorem DescriptiveComplexity.StepDef.inflStage_eq_limit_of_stratGate {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] [Finite A] {n m : ℕ} (hnm : n ≤ m) (h : StratGate ((d₁.stratify d₂).inflStage A n)) : d₁.inflStage A m = d₁.inflLimit A

While the gate is on, the first stratum sits at its limit.

theorem DescriptiveComplexity.StepDef.next_stratify_inr {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] (σ : (stratBlock d₁.B d₂.B).Assignment A) (i : d₂.B.ι) (x : Fin (d₂.B.arity i) → A) : (d₁.stratify d₂).next σ (Sum.inr i) x ↔ StratGate σ ∧ (d₂.step i).Realize x

One step of the second stratum, decomposed: the gate at the current stage, and the second stratum's own step over the frozen strata.

theorem DescriptiveComplexity.StepDef.strat2Assign_inflStage_succ_of_not_stratGate {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] {n : ℕ} (h : ¬StratGate ((d₁.stratify d₂).inflStage A n)) : strat2Assign ((d₁.stratify d₂).inflStage A (n + 1)) = strat2Assign ((d₁.stratify d₂).inflStage A n)

While the gate is off, the second stratum does not move.

theorem DescriptiveComplexity.StepDef.strat2Assign_eq_bot_of_not_stratGate {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] {n : ℕ} (h : ¬StratGate ((d₁.stratify d₂).inflStage A n)) : strat2Assign ((d₁.stratify d₂).inflStage A n) = d₂.B.botAssign A

While the gate is off, the second stratum is empty.

theorem DescriptiveComplexity.StepDef.strat2Assign_inflStage_add {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] [Finite A] {G : ℕ} (hG : StratGate ((d₁.stratify d₂).inflStage A G)) (hGmin : ∀ m < G, ¬StratGate ((d₁.stratify d₂).inflStage A m)) (m : ℕ) : strat2Assign ((d₁.stratify d₂).inflStage A (G + m)) = d₂.inflStage A m

The second stratum replays its own stages once the gate fires: from the first gate-on stage, the second-stratum parts are the stages of the second stratum over the structure expanded by the first stratum's limit.

theorem DescriptiveComplexity.StepDef.strat2Assign_inflLimit {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] [Finite A] : strat2Assign ((d₁.stratify d₂).inflLimit A) = d₂.inflLimit A

The second-stratum part of the composite limit is the second stratum's own limit over the structure expanded by the first stratum's limit.

theorem DescriptiveComplexity.StepDef.strat1Assign_inflLimit {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] : strat1Assign ((d₁.stratify d₂).inflLimit A) = d₁.inflLimit A

The first-stratum part of the composite limit is the first stratum's own limit.

theorem DescriptiveComplexity.StepDef.ifpHolds_stratify {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] [Finite A] : (d₁.stratify d₂).IFPHolds A ↔ d₂.IFPHolds A

Stratification: the value of the stratified induction is the value of the second stratum, read over the structure expanded by the first stratum's limit. Nested inflationary inductions are one induction.