Numbers computed by a tower

A family of numbers (DescriptiveComplexity.Digits.Fam) attaches a number to each tuple of parameters of each ordered structure. Its digit relation (DescriptiveComplexity.Digits.digRel) holds of the parameters followed by a position – an ℓ-tuple – when the digit of that position is 1.

DescriptiveComplexity.Digits.Dig e₀ ℓ F says that the digit relation of F can be added to any tower above the induction e₀: whatever the induction extending e₀, one more extension computes it. Stating it over every extension is what lets the constructions be chained, each starting from the tower the previous one left.

This file holds the two ways of adding a relation to a tower – by a formula (DescriptiveComplexity.Digits.exists_ext_of_formula) and by a sweep (DescriptiveComplexity.Digits.exists_ext_of_sweep) – and the first closure property, under addition (DescriptiveComplexity.Digits.Dig.add).

@[reducible, inline]

abbrev DescriptiveComplexity.Digits.Fam (K : FirstOrder.Language) (a : ℕ) : Type 1

A family of numbers: one for each tuple of a parameters of each ordered structure.

Equations

• DescriptiveComplexity.Digits.Fam K a = ((A : Type) → [K.Structure A] → [LinearOrder A] → (Fin a → A) → ℕ)

def DescriptiveComplexity.Digits.digRel {K : FirstOrder.Language} (ℓ : ℕ) {a : ℕ} (F : Fam K a) (A : Type) [K.Structure A] [LinearOrder A] : (Fin (a + ℓ) → A) → Prop

The digit relation of a family of numbers: the parameters, followed by the positions of the digits 1.

Equations

• DescriptiveComplexity.Digits.digRel ℓ F A x = DescriptiveComplexity.Digits.tupBits (F A fun (k : Fin a) => x (Fin.castAdd ℓ k)) fun (k : Fin ℓ) => x (Fin.natAdd a k)

@[reducible, inline]

abbrev DescriptiveComplexity.Digits.ctxStr {K : FirstOrder.Language} (e : StepDef (K.sum FirstOrder.Language.order)) (A : Type) [K.Structure A] [LinearOrder A] : ((K.sum FirstOrder.Language.order).sum e.B.lang).Structure A

The structure a stratum above an induction reads: the ordered structure, expanded by the limit of the induction.

Equations

• DescriptiveComplexity.Digits.ctxStr e A = e.B.structure₁ (e.inflLimit A)

Reading a relation of the tower

def DescriptiveComplexity.Digits.ctxAt {K : FirstOrder.Language} {e : StepDef (K.sum FirstOrder.Language.order)} {γ : Type} {r : ℕ} (j : e.B.lang.Relations r) (ts : Fin r → γ) : ((K.sum FirstOrder.Language.order).sum e.B.lang).Formula γ

An atom of a relation variable of the induction.

Equations

• DescriptiveComplexity.Digits.ctxAt j ts = FirstOrder.Language.Relations.formula (Sum.inr j) fun (k : Fin r) => FirstOrder.Language.var (ts k)

def DescriptiveComplexity.Digits.numAt {K : FirstOrder.Language} {e : StepDef (K.sum FirstOrder.Language.order)} {ℓ : ℕ} {γ : Type} {a : ℕ} (j : e.B.lang.Relations (a + ℓ)) (ws : Fin a → γ) : ((K.sum FirstOrder.Language.order).sum e.B.lang).Formula (γ ⊕ Fin ℓ)

The number computed by a relation variable, at given parameters: a formula of the position.

Equations

• DescriptiveComplexity.Digits.numAt j ws = DescriptiveComplexity.Digits.ctxAt j (Fin.append (fun (i : Fin a) => Sum.inl (ws i)) Sum.inr)

Adding a relation to a tower

theorem DescriptiveComplexity.Digits.exists_ext_of_formula {K : FirstOrder.Language} (e : StepDef (K.sum FirstOrder.Language.order)) {r : ℕ} (ψ : ((K.sum FirstOrder.Language.order).sum e.B.lang).Formula (Fin r)) (R : (A : Type) → [K.Structure A] → [LinearOrder A] → (Fin r → A) → Prop) (h : ∀ (A : Type) [inst : K.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (x : Fin r → A), ψ.Realize x ↔ R A x) : ∃ (e' : StepDef (K.sum FirstOrder.Language.order)) (x : e.Ext e') (j : e'.B.lang.Relations r), e'.Computes j R

A relation defined by a formula over a tower is computed by an extension of it.

theorem DescriptiveComplexity.Digits.exists_ext_of_sweep {K : FirstOrder.Language} (e : StepDef (K.sum FirstOrder.Language.order)) {a q ℓ : ℕ} (bot : ((K.sum FirstOrder.Language.order).sum e.B.lang).Formula (Fin q)) (cov : ((K.sum FirstOrder.Language.order).sum e.B.lang).Formula (Fin q ⊕ Fin q)) (Θ : (((K.sum FirstOrder.Language.order).sum e.B.lang).sum (sweepBlock a q ℓ).lang).Formula ((Fin a ⊕ Fin q) ⊕ Fin ℓ)) (T : (A : Type) → [K.Structure A] → [LinearOrder A] → (Fin (a + q + ℓ) → A) → Prop) (h : ∀ (A : Type) [inst : K.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (w : Fin a → A) (i : Fin q → A) (p : Fin ℓ → A), (sweep bot cov Θ).inflLimit A true (j3 w i p) ↔ T A (j3 w i p)) : ∃ (e' : StepDef (K.sum FirstOrder.Language.order)) (x : e.Ext e') (j : e'.B.lang.Relations (a + q + ℓ)), e'.Computes j T

The rows of a sweep over a tower are computed by an extension of it.

Numbers that can be added to any tower

def DescriptiveComplexity.Digits.Dig {K : FirstOrder.Language} (e₀ : StepDef (K.sum FirstOrder.Language.order)) (ℓ : ℕ) {a : ℕ} (F : Fam K a) : Prop

The digits of the family F can be added to any tower above e₀.

Equations

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

theorem DescriptiveComplexity.Digits.Dig.congr {K : FirstOrder.Language} {e₀ : StepDef (K.sum FirstOrder.Language.order)} {ℓ a : ℕ} {F G : Fam K a} (h : ∀ (A : Type) [inst : K.Structure A] [inst_1 : LinearOrder A] (w : Fin a → A), F A w = G A w) (hF : Dig e₀ ℓ F) : Dig e₀ ℓ G

Families with the same values.

theorem DescriptiveComplexity.Digits.Dig.of_base {K : FirstOrder.Language} {e₀ : StepDef (K.sum FirstOrder.Language.order)} {ℓ a : ℕ} (F : Fam K a) (ψ : (K.sum FirstOrder.Language.order).Formula (Fin a ⊕ Fin ℓ)) (h : ∀ (A : Type) [inst : K.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A] (w : Fin a → A) (p : Fin ℓ → A), ψ.Realize (Sum.elim w p) ↔ tupBits (F A w) p) : Dig e₀ ℓ F

A family defined by a formula of the ordered vocabulary alone.

theorem DescriptiveComplexity.Digits.Dig.zero {K : FirstOrder.Language} {e₀ : StepDef (K.sum FirstOrder.Language.order)} {ℓ : ℕ} (a : ℕ) : Dig e₀ ℓ fun (x : Type) (x_1 : K.Structure x) (x_2 : LinearOrder x) (x_3 : Fin a → x) => 0

The family constantly zero.

theorem DescriptiveComplexity.Digits.Dig.one {K : FirstOrder.Language} {e₀ : StepDef (K.sum FirstOrder.Language.order)} {ℓ : ℕ} (a : ℕ) : Dig e₀ ℓ fun (x : Type) (x_1 : K.Structure x) (x_2 : LinearOrder x) (x_3 : Fin a → x) => 1

The family constantly one.

theorem DescriptiveComplexity.Digits.Dig.add {K : FirstOrder.Language} {e₀ : StepDef (K.sum FirstOrder.Language.order)} {ℓ a : ℕ} {F G : Fam K a} (hF : Dig e₀ ℓ F) (hG : Dig e₀ ℓ G) : Dig e₀ ℓ fun (A : Type) (x : K.Structure A) (x_1 : LinearOrder A) (w : Fin a → A) => F A w + G A w

Closure under addition: the sum of two numbers is defined by carry lookahead from their digits.