The digits of a quantitative term

DescriptiveComplexity.Digits.dig_term: the binary digits of the value of a term of quantitative first-order logic, read over the structure expanded by the limit of an induction e₀, can be added to any tower above e₀. By induction on the term, each construct being one closure property:

• a formula, counting 1 or 0: one first-order stratum, the formula being read in the tower through the embedding of e₀;
• a constant: iterated addition of ones;
• + and ·: DescriptiveComplexity.Digits.Dig.add, DescriptiveComplexity.Digits.Dig.mul;
• Σx̄ and Πx̄: DescriptiveComplexity.Digits.Dig.sum, DescriptiveComplexity.Digits.Dig.prod, the bound variables becoming parameters.

The digits are those of the value modulo 2 ^ (n ^ ℓ), for any ℓ; no bound on the value is needed here.

noncomputable def DescriptiveComplexity.Digits.termFam {K : FirstOrder.Language} (e₀ : StepDef (K.sum FirstOrder.Language.order)) {α : Type} (t : QTerm ((K.sum FirstOrder.Language.order).sum e₀.B.lang) α) {a : ℕ} (f : α → Fin a) : Fam K a

The value of a term, as a family of numbers: its free variables are read off the parameters through f.

Equations

• DescriptiveComplexity.Digits.termFam e₀ t f A w = t.eval fun (y : α) => w (f y)

theorem DescriptiveComplexity.Digits.dig_term {K : FirstOrder.Language} {e₀ : StepDef (K.sum FirstOrder.Language.order)} (ℓ : ℕ) {α : Type} (t : QTerm ((K.sum FirstOrder.Language.order).sum e₀.B.lang) α) {a : ℕ} (f : α → Fin a) : Dig e₀ ℓ (termFam e₀ t f)

The digits of the value of a term can be added to any tower.