Closure under sums over the tuples of the structure

DescriptiveComplexity.Digits.Dig.sum: if the digits of a family F of numbers, with parameters w̄ and ū, can be added to a tower, so can the digits of Σū. F(w̄, ū).

The sum is an iterated addition, computed by a sweep (DescriptiveComplexity.Digits.sweep) along the tuples ū in lexicographic order: the row of ū holds the digits of the sum of F up to ū (DescriptiveComplexity.Digits.sumFam), and is the sum, by carry lookahead, of the row before it and of F(w̄, ū) (DescriptiveComplexity.Digits.sumTheta). The answer is the row of the last tuple.

Variables in two blocks

def DescriptiveComplexity.Digits.u2 {a m : ℕ} : Fin (a + m) → Fin a ⊕ Fin m

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

Equations

• DescriptiveComplexity.Digits.u2 k = Fin.addCases Sum.inl Sum.inr k

The lexicographic order on tuples, as sweep data

noncomputable def DescriptiveComplexity.Digits.lexBotF {K : FirstOrder.Language} (e : StepDef (K.sum FirstOrder.Language.order)) (m : ℕ) : ((K.sum FirstOrder.Language.order).sum e.B.lang).Formula (Fin m)

“The tuple is the least one.”

Equations

• DescriptiveComplexity.Digits.lexBotF e m = FirstOrder.Language.LHom.sumInl.onFormula (DescriptiveComplexity.minTupF id)

noncomputable def DescriptiveComplexity.Digits.lexCovF {K : FirstOrder.Language} (e : StepDef (K.sum FirstOrder.Language.order)) (m : ℕ) : ((K.sum FirstOrder.Language.order).sum e.B.lang).Formula (Fin m ⊕ Fin m)

“The second tuple covers the first.”

Equations

• DescriptiveComplexity.Digits.lexCovF e m = FirstOrder.Language.LHom.sumInl.onFormula (DescriptiveComplexity.succTupF Sum.inl Sum.inr)

The rows: partial sums

@[reducible, inline]

abbrev DescriptiveComplexity.Digits.sweepHom {K : FirstOrder.Language} (e : StepDef (K.sum FirstOrder.Language.order)) (a q ℓ : ℕ) : K.sum FirstOrder.Language.order →ᴸ ((K.sum FirstOrder.Language.order).sum e.B.lang).sum (sweepBlock a q ℓ).lang

The ordered vocabulary, read in the vocabulary of a sweep over a tower.

Equations

• DescriptiveComplexity.Digits.sweepHom e a q ℓ = FirstOrder.Language.LHom.sumInl.comp FirstOrder.Language.LHom.sumInl

noncomputable def DescriptiveComplexity.Digits.sumTheta {K : FirstOrder.Language} {e : StepDef (K.sum FirstOrder.Language.order)} {a m ℓ : ℕ} (jF : e.B.lang.Relations (a + m + ℓ)) : (((K.sum FirstOrder.Language.order).sum e.B.lang).sum (sweepBlock a m ℓ).lang).Formula ((Fin a ⊕ Fin m) ⊕ Fin ℓ)

The row of a tuple: the digits of the family at the least tuple, and otherwise the sum of the row before and of the digits of the family.

Equations

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

Closure

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

Closure under sums over tuples.