An induction, then a partial iteration: one partial iteration

DescriptiveComplexity.StepDef.stratify composes two inflationary inductions. This file composes an inflationary induction with a partial one (DescriptiveComplexity.StepDef.stratifyPFP): the value of the second iteration, run over the structure expanded by the first one's limit, is the value of a single partial iteration (DescriptiveComplexity.StepDef.pfpHolds_stratifyPFP).

That is what closes DescriptiveComplexity.PSPACE under FO(LFP) reductions (DescriptiveComplexity.FixedPointReductionSpace): a reduction's induction has to be absorbed into the membership witness, and PSPACE's witness is a partial iteration.

Why a partial second stratum still works

The received reason to expect trouble is that a partial iteration is not monotone, so “run the second stratum once the first has converged” cannot be arranged by inflation, as DescriptiveComplexity.StepDef.stratify arranges it. What makes it work anyway is that only the gating needs monotonicity, and the gate is a bit of the state, not of the second stratum:

• the first stratum's variables accumulate – its step formula is written with the accumulation spelled out, since the composite iteration replaces rather than accumulates;
• the gate is an arity-0 variable, set once the first stratum's step formulas add nothing (DescriptiveComplexity.stratGateF) and never unset;
• the second stratum's step is conjoined with the gate, so its variables stay empty until the gate fires and then iterate partially, from the empty assignment, over the frozen first stratum.

The stage count then shifts by the gate's index and nothing else: the composite is at stage G + 1 + m exactly what the second stratum is at stage m (DescriptiveComplexity.StepDef.strat2Assign_partStage_add). Fixed points can only occur after the gate has fired – before it, either the first stratum still moves or the gate itself does – so the composite converges exactly when the second stratum does, and reads the same output there.

The atom of a first-stratum variable

noncomputable def DescriptiveComplexity.strat1AtomF (L : FirstOrder.Language) (B₁ B₂ : SOBlock) (i : B₁.ι) : (L.sum (stratBlock B₁ B₂).lang).Formula (Fin (B₁.arity i))

A first-stratum variable, as a formula over the combined block: the composite iteration replaces rather than accumulates, so the accumulation has to be written out.

Equations

• DescriptiveComplexity.strat1AtomF L B₁ B₂ i = (DescriptiveComplexity.strat1Sym L B₁ B₂ i).formula fun (j : Fin (B₁.arity i)) => FirstOrder.Language.var j

theorem DescriptiveComplexity.realize_strat1AtomF {L : FirstOrder.Language} {B₁ B₂ : SOBlock} {A : Type} [L.Structure A] (σ : (stratBlock B₁ B₂).Assignment A) (i : B₁.ι) (x : Fin (B₁.arity i) → A) : (strat1AtomF L B₁ B₂ i).Realize x ↔ strat1Assign σ i x

The composite

@[reducible]

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

An inflationary stratum followed by a partial one: the first stratum's variables accumulate, the gate fires when they stop moving, and the second stratum's variables iterate partially behind the gate, over the frozen first stratum.

Reducible, so that the block of the composite is the combined block: the stage lemmas below rewrite with assignment-level equalities, which instance search must see through.

Equations

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

theorem DescriptiveComplexity.StepDef.next_stratifyPFP_inl {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₁.stratifyPFP d₂).next σ (Sum.inl (Sum.inl i)) x ↔ strat1Assign σ i x ∨ d₁.next (strat1Assign σ) i x

One step of the first stratum: its own inflationary step, the accumulation being written out.

theorem DescriptiveComplexity.StepDef.next_stratifyPFP_gate {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) : (d₁.stratifyPFP d₂).next σ (Sum.inl (Sum.inr ())) Fin.elim0 ↔ StratGate σ ∨ ∀ (i : d₁.B.ι) (x : Fin (d₁.B.arity i) → A), d₁.next (strat1Assign σ) i x → strat1Assign σ i x

One step of the gate: set once the first stratum's steps add nothing, and never unset.

theorem DescriptiveComplexity.StepDef.next_stratifyPFP_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) (j : d₂.B.ι) (x : Fin (d₂.B.arity j) → A) : (d₁.stratifyPFP d₂).next σ (Sum.inr j) x ↔ StratGate σ ∧ (d₂.step j).Realize x

One step of the second stratum: empty until the gate fires, one partial step over the frozen first stratum afterwards.

The three parts of one step

theorem DescriptiveComplexity.StepDef.strat1Assign_next_stratifyPFP {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) : strat1Assign ((d₁.stratifyPFP d₂).next σ) = d₁.inflStep (strat1Assign σ)

The first stratum of one step is its own inflationary step.

theorem DescriptiveComplexity.StepDef.stratGate_next_stratifyPFP {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) : StratGate ((d₁.stratifyPFP d₂).next σ) ↔ StratGate σ ∨ Function.IsFixedPt d₁.inflStep (strat1Assign σ)

The gate of one step.

theorem DescriptiveComplexity.StepDef.strat2Assign_next_stratifyPFP {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) : strat2Assign ((d₁.stratifyPFP d₂).next σ) = fun (j : d₂.B.ι) (x : Fin (d₂.B.arity j) → A) => StratGate σ ∧ d₂.next (strat2Assign σ) j x

The second stratum of one step.

The stages of the composite

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

The first stratum of the composite stages is its own inflationary stages.

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

The gate of the composite stages: it turns on when the first stratum stops moving, and never off.

theorem DescriptiveComplexity.StepDef.not_stratGate_partStage_zero {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] : ¬StratGate ((d₁.stratifyPFP d₂).partStage A 0)

The gate is off at the start.

theorem DescriptiveComplexity.StepDef.stratGate_partStage_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₁.stratifyPFP d₂).partStage A m)) : StratGate ((d₁.stratifyPFP d₂).partStage A n)

The gate stays on.

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

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

theorem DescriptiveComplexity.StepDef.strat2Assign_partStage_add {L : FirstOrder.Language} (d₁ : StepDef L) (d₂ : StepDef (L.sum d₁.B.lang)) {A : Type} [L.Structure A] {G : ℕ} {ρ₁ : d₁.B.Assignment A} (hG : StratGate ((d₁.stratifyPFP d₂).partStage A G)) (hbot : strat2Assign ((d₁.stratifyPFP d₂).partStage A G) = d₂.B.botAssign A) (hfr : ∀ (n : ℕ), G ≤ n → strat1Assign ((d₁.stratifyPFP d₂).partStage A n) = ρ₁) (m : ℕ) : strat2Assign ((d₁.stratifyPFP d₂).partStage A (G + m)) = d₂.partStage A m

Once the gate is on and the first stratum frozen, the second stratum replays its own partial stages.

The value of the composite

theorem DescriptiveComplexity.StepDef.inflLimit_eq_inflStage_of_isFixedPt {L : FirstOrder.Language} (d₁ : StepDef L) {A : Type} [L.Structure A] {k : ℕ} (h : Function.IsFixedPt d₁.inflStep (d₁.inflStage A k)) : d₁.inflLimit A = d₁.inflStage A k

An inflationary limit is reached at any stage that stops moving.

theorem DescriptiveComplexity.StepDef.stratBlock_ext {A : Type} {B₁ B₂ : SOBlock} {σ τ : (stratBlock B₁ B₂).Assignment A} (h1 : strat1Assign σ = strat1Assign τ) (hg : StratGate σ ↔ StratGate τ) (h2 : strat2Assign σ = strat2Assign τ) : σ = τ

An assignment of the combined block is its three parts.

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

The composite computes the second iteration over the first one's limit. An inflationary induction followed by a partial iteration is one partial iteration: the composite converges exactly when the second stratum does, over the structure expanded by the first stratum's limit, and reads the same output there.