The size of the value of a quantitative term

Two facts about a term of quantitative first-order logic (DescriptiveComplexity.QTerm), needed to write its value digit by digit.

• A polynomial number of digits (DescriptiveComplexity.QTerm.exists_bound): for some ℓ, the value is below 2 ^ (n ^ ℓ) on every structure with n ≥ 2 elements. So the ℓ-tuples of elements are enough positions for its binary digits.
• One-element structures (DescriptiveComplexity.QTerm.exists_formulas): there, a term takes finitely many values, and “the value is N” is a formula. A one-element structure has a single tuple of each length, hence too few positions, and is treated apart.

A polynomial number of digits

theorem DescriptiveComplexity.QTerm.exp_mono {n : ℕ} (hn : 2 ≤ n) {a b : ℕ} (h : a ≤ b) : 2 ^ n ^ a ≤ 2 ^ n ^ b

theorem DescriptiveComplexity.QTerm.exists_bound {L : FirstOrder.Language} {α : Type} (t : QTerm L α) : ∃ (ℓ : ℕ), ∀ (A : Type) [inst : L.Structure A] [Finite A], 2 ≤ Nat.card A → ∀ (v : α → A), t.eval v < 2 ^ Nat.card A ^ ℓ

The value of a term has polynomially many digits: it is below 2 ^ (n ^ ℓ) on the structures with n ≥ 2 elements.

One-element structures

theorem DescriptiveComplexity.QTerm.exists_formulas {L : FirstOrder.Language} {α : Type} (t : QTerm L α) : ∃ (M : ℕ) (χ : ℕ → L.Formula α), ∀ (A : Type) [inst : L.Structure A] [Subsingleton A] [Nonempty A] (v : α → A), t.eval v ≤ M ∧ ∀ (N : ℕ), (χ N).Realize v ↔ t.eval v = N

On one-element structures a term takes finitely many values, each recognized by a formula.