Towers of inductions: first-order strata and sweep strata

The definability layer of the normal form of FP (DescriptiveComplexity.Counting.Digits). The digits of a quantitative term are computed by a tower of inflationary inductions, each reading the converged relations of the ones below as if they were relations of the instance; a tower is one induction, by stratification (DescriptiveComplexity.StepDef.stratify). Two kinds of stratum are all the construction uses, and both are stated over an arbitrary vocabulary M – in a tower, the base vocabulary expanded by the relations already computed:

• a first-order stratum (DescriptiveComplexity.Digits.foStratum) defines a family of relations by formulas of M; its limit is what the formulas say (DescriptiveComplexity.Digits.inflLimit_foStratum);
• a sweep stratum (DescriptiveComplexity.Digits.sweep) computes rows indexed by the tuples of a definable linear order, each row by a formula that may read the rows before it. It is the iteration of DescriptiveComplexity.Digits.sweep_limit, written with a relation done beside the relation row, and its limit is the family of rows (DescriptiveComplexity.Digits.inflLimit_sweep).

DescriptiveComplexity.StepDef.Ext is the bookkeeping of a tower: an induction extends another when it computes, among others, the same relations.

Tuples in blocks

def DescriptiveComplexity.Digits.j3 {A : Type} {a q ℓ : ℕ} (w : Fin a → A) (i : Fin q → A) (p : Fin ℓ → A) : Fin (a + q + ℓ) → A

Parameters, then an index, then a position.

Equations

• DescriptiveComplexity.Digits.j3 w i p = Fin.append (Fin.append w i) p

def DescriptiveComplexity.Digits.g2 {a q : ℕ} : Fin a ⊕ Fin q → Fin (a + q)

The variables of a formula about parameters and an index, as arguments of a relation.

Equations

• DescriptiveComplexity.Digits.g2 = Sum.elim (Fin.castAdd q) (Fin.natAdd a)

def DescriptiveComplexity.Digits.g3 {a q ℓ : ℕ} : (Fin a ⊕ Fin q) ⊕ Fin ℓ → Fin (a + q + ℓ)

The variables of a formula about parameters, an index and a position, as arguments of a relation.

Equations

• DescriptiveComplexity.Digits.g3 = Sum.elim (Fin.castAdd ℓ ∘ DescriptiveComplexity.Digits.g2) (Fin.natAdd (a + q))

First-order strata

@[reducible]

noncomputable def DescriptiveComplexity.Digits.foStratum {M : FirstOrder.Language} (J : Type) [Finite J] (ar : J → ℕ) (ψ : (j : J) → M.Formula (Fin (ar j))) : StepDef M

A first-order stratum: a family of relations, each defined by a formula of the vocabulary.

Equations

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

theorem DescriptiveComplexity.Digits.inflLimit_foStratum {M : FirstOrder.Language} {A : Type} [M.Structure A] (J : Type) [Finite J] (ar : J → ℕ) (ψ : (j : J) → M.Formula (Fin (ar j))) (j : J) (x : Fin (ar j) → A) : (foStratum J ar ψ).inflLimit A j x ↔ (ψ j).Realize x

The limit of a first-order stratum is what its formulas say.

Sweep strata

@[reducible]

def DescriptiveComplexity.Digits.sweepBlock (a q ℓ : ℕ) : SOBlock

The block of a sweep: the relation row (parameters, index, position) and the relation done (parameters, index).

Equations

• DescriptiveComplexity.Digits.sweepBlock a q ℓ = { ι := Bool, ιFinite := Bool.instFinite, arity := fun (b : Bool) => bif b then a + q + ℓ else a + q }

@[reducible, inline]

abbrev DescriptiveComplexity.Digits.rowSym (M : FirstOrder.Language) (a q ℓ : ℕ) : (M.sum (sweepBlock a q ℓ).lang).Relations (a + q + ℓ)

The symbol of the rows.

Equations

• DescriptiveComplexity.Digits.rowSym M a q ℓ = Sum.inr ⟨true, ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.Digits.doneSym (M : FirstOrder.Language) (a q ℓ : ℕ) : (M.sum (sweepBlock a q ℓ).lang).Relations (a + q)

The symbol of the marker.

Equations

• DescriptiveComplexity.Digits.doneSym M a q ℓ = Sum.inr ⟨false, ⋯⟩

def DescriptiveComplexity.Digits.doneAt {M : FirstOrder.Language} {a q : ℕ} (ℓ : ℕ) {γ : Type} (ws : Fin a → γ) (is : Fin q → γ) : (M.sum (sweepBlock a q ℓ).lang).Formula γ

“The row of this index is done.”

Equations

• DescriptiveComplexity.Digits.doneAt ℓ ws is = (DescriptiveComplexity.Digits.doneSym M a q ℓ).formula fun (k : Fin (a + q)) => FirstOrder.Language.var (Fin.append ws is k)

def DescriptiveComplexity.Digits.rowAt {M : FirstOrder.Language} {a q ℓ : ℕ} {γ : Type} (ws : Fin a → γ) (is : Fin q → γ) (ps : Fin ℓ → γ) : (M.sum (sweepBlock a q ℓ).lang).Formula γ

“This position is in the row of this index.”

Equations

• DescriptiveComplexity.Digits.rowAt ws is ps = (DescriptiveComplexity.Digits.rowSym M a q ℓ).formula fun (k : Fin (a + q + ℓ)) => FirstOrder.Language.var (Fin.append (Fin.append ws is) ps k)

noncomputable def DescriptiveComplexity.Digits.readyF {M : FirstOrder.Language} {a q : ℕ} (ℓ : ℕ) (bot : M.Formula (Fin q)) (cov : M.Formula (Fin q ⊕ Fin q)) : (M.sum (sweepBlock a q ℓ).lang).Formula (Fin a ⊕ Fin q)

“The row of this index may be written”: the index is the first one, or the row of the index it covers is done.

Equations

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

@[reducible]

noncomputable def DescriptiveComplexity.Digits.sweep {M : FirstOrder.Language} {a q ℓ : ℕ} (bot : M.Formula (Fin q)) (cov : M.Formula (Fin q ⊕ Fin q)) (Θ : (M.sum (sweepBlock a q ℓ).lang).Formula ((Fin a ⊕ Fin q) ⊕ Fin ℓ)) : StepDef M

A sweep stratum: rows indexed by the tuples of a linear order given by its least element (bot) and its covers (cov), each row defined by the formula Θ – about parameters, an index and a position – which may read the rows before it.

Equations

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

theorem DescriptiveComplexity.Digits.inflLimit_sweep {M : FirstOrder.Language} {a q ℓ : ℕ} {A : Type} [M.Structure A] {Idx : Type} [LinearOrder Idx] [Finite Idx] (ix : (Fin q → A) ≃ Idx) (bot : M.Formula (Fin q)) (cov : M.Formula (Fin q ⊕ Fin q)) (Θ : (M.sum (sweepBlock a q ℓ).lang).Formula ((Fin a ⊕ Fin q) ⊕ Fin ℓ)) (hbot : ∀ (i : Fin q → A), bot.Realize i ↔ ∀ (c : Idx), ix i ≤ c) (hcov : ∀ (i₀ i : Fin q → A), cov.Realize (Sum.elim i₀ i) ↔ ix i₀ ⋖ ix i) (Φ : (Fin a → A) → Idx → (Idx → (Fin ℓ → A) → Prop) → (Fin ℓ → A) → Prop) (T : (Fin a → A) → Idx → (Fin ℓ → A) → Prop) (hΦ : ∀ (w : Fin a → A) (i : Idx) (R : Idx → (Fin ℓ → A) → Prop), (∀ i' < i, R i' = T w i') → Φ w i R = T w i) (hΘ : ∀ (ρ : (sweepBlock a q ℓ).Assignment A) (w : Fin a → A) (i : Fin q → A) (p : Fin ℓ → A), Θ.Realize (Sum.elim (Sum.elim w i) p) ↔ Φ w (ix i) (fun (i' : Idx) (p' : Fin ℓ → A) => ρ true (j3 w (ix.symm i') p')) p) (w : Fin a → A) (i : Fin q → A) (p : Fin ℓ → A) : (sweep bot cov Θ).inflLimit A true (j3 w i p) ↔ T w (ix i) p

The limit of a sweep stratum is the family of its rows. The index tuples are read as the elements of a finite linear order through ix; the formula Θ realizes a condition Φ on the rows, which determines the row of an index from the rows before it.

Extensions

structure DescriptiveComplexity.StepDef.Ext {K : FirstOrder.Language} (e e' : StepDef (K.sum FirstOrder.Language.order)) : Type

An induction extends another when it computes, among others, the same relations: a map of the relation variables, preserving the arities and the limits.

• emb : e.B.ι → e'.B.ι

  Where a relation variable of the first induction is in the second.

• arity_emb (i : e.B.ι) : e'.B.arity (self.emb i) = e.B.arity i

  The arities are preserved.

• limit (A : Type) [K.Structure A] [LinearOrder A] [Finite A] : SOBlock.homAssign self.emb ⋯ (e'.inflLimit A) = e.inflLimit A

  The limits are preserved.

def DescriptiveComplexity.StepDef.Ext.refl {K : FirstOrder.Language} (e : StepDef (K.sum FirstOrder.Language.order)) : e.Ext e

Every induction extends itself.

Equations

• DescriptiveComplexity.StepDef.Ext.refl e = { emb := id, arity_emb := ⋯, limit := ⋯ }

def DescriptiveComplexity.StepDef.Ext.trans {K : FirstOrder.Language} {e e' e'' : StepDef (K.sum FirstOrder.Language.order)} (x : e.Ext e') (y : e'.Ext e'') : e.Ext e''

Extensions compose.

Equations

• x.trans y = { emb := y.emb ∘ x.emb, arity_emb := ⋯, limit := ⋯ }

noncomputable def DescriptiveComplexity.StepDef.Ext.stratify {K : FirstOrder.Language} (e : StepDef (K.sum FirstOrder.Language.order)) (d : StepDef ((K.sum FirstOrder.Language.order).sum e.B.lang)) : e.Ext (e.stratify d)

Adding a stratum extends an induction.

Equations

• DescriptiveComplexity.StepDef.Ext.stratify e d = { emb := fun (i : e.B.ι) => Sum.inl (Sum.inl i), arity_emb := ⋯, limit := ⋯ }

def DescriptiveComplexity.StepDef.Ext.sym {K : FirstOrder.Language} {e e' : StepDef (K.sum FirstOrder.Language.order)} (x : e.Ext e') {r : ℕ} (j : e.B.lang.Relations r) : e'.B.lang.Relations r

The symbol of a relation variable, in an extension.

Equations

• x.sym j = ⟨x.emb ↑j, ⋯⟩

def DescriptiveComplexity.StepDef.Computes {K : FirstOrder.Language} (e : StepDef (K.sum FirstOrder.Language.order)) {r : ℕ} (j : e.B.lang.Relations r) (R : (A : Type) → [K.Structure A] → [LinearOrder A] → (Fin r → A) → Prop) : Prop

The relation variable j of the induction e computes the relation R of ordered structures.

Equations

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

theorem DescriptiveComplexity.StepDef.Computes.ext {K : FirstOrder.Language} {e e' : StepDef (K.sum FirstOrder.Language.order)} {r : ℕ} {j : e.B.lang.Relations r} {R : (A : Type) → [K.Structure A] → [LinearOrder A] → (Fin r → A) → Prop} (h : e.Computes j R) (x : e.Ext e') : e'.Computes (x.sym j) R

theorem DescriptiveComplexity.StepDef.inflLimit_stratify_inr {K : FirstOrder.Language} (e : StepDef (K.sum FirstOrder.Language.order)) (d : StepDef ((K.sum FirstOrder.Language.order).sum e.B.lang)) (A : Type) [K.Structure A] [LinearOrder A] [Finite A] (i : d.B.ι) (x : Fin (d.B.arity i) → A) : (e.stratify d).inflLimit A (Sum.inr i) x ↔ d.inflLimit A i x

The relations of a new stratum, in the stratified induction: their limits are those of the stratum, over the structure expanded by the limit of the induction below.