Closure under products over the tuples of the structure

DescriptiveComplexity.Digits.Dig.prod: if the digits of a family I of numbers with parameters w̄, and of a family F with parameters w̄ and ū, can be added to a tower, so can the digits of I(w̄) · Πū. F(w̄, ū). With one tuple ū only, this is closure under multiplication (DescriptiveComplexity.Digits.Dig.mul).

The semantics is DescriptiveComplexity.Counting.Digits.ProdSem: one sweep along the pairs of a tuple and a position. What is here is the formula of a row (DescriptiveComplexity.Digits.prodTheta), the order of the sweep as formulas (DescriptiveComplexity.Digits.prodBotF, DescriptiveComplexity.Digits.prodCovF), and the reading of the answer off the last row.

The order of the sweep

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

“The index is the first one”: the least tuple, at the greatest position.

Equations

• DescriptiveComplexity.Digits.prodBotF e m ℓ = FirstOrder.Language.LHom.sumInl.onFormula (DescriptiveComplexity.minTupF (Fin.castAdd ℓ) ⊓ DescriptiveComplexity.maxTupF (Fin.natAdd m))

noncomputable def DescriptiveComplexity.Digits.prodCovF {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 index follows the first”: the same tuple at the position just below, or the next tuple at the greatest position, from the least one.

Equations

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

The rows

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

The product before the tuple of the index: the initial number at the least tuple, the last row of the previous tuple otherwise.

Equations

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

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

The previous row of the same tuple: the row of the position just above.

Equations

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

noncomputable def DescriptiveComplexity.Digits.prodTheta {K : FirstOrder.Language} {e : StepDef (K.sum FirstOrder.Language.order)} {a m ℓ : ℕ} (jI : e.B.lang.Relations (a + ℓ)) (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 an index: the double of the previous row of the tuple, plus the product before the tuple when the digit of the factor is 1.

Equations

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

Closure

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

Closure under products over tuples, with an initial factor.

theorem DescriptiveComplexity.Digits.Dig.mul {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 multiplication: a product over the one tuple of length zero.