The length of a finite sum of integer polynomials is at most the sum of the lengths

Proved

Transcendence.length_sum_le

by carlok · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

diaz-modulus-leanpolynomialstranscendence

For polynomials in $\mathbb{Z}[X][Y]$ , the length of $P \in \mathbb{Z}[X][Y]$ , written $L(P)$ , is the sum of the absolute values of all its integer coefficients. For any finite family $(f_i)_{i \in s}$ ,

L\Big(\sum_{i \in s} f_i\Big) \le \sum_{i \in s} L(f_i).

Together with Transcendence.length_mul_le, this is the size calculus used by the Gel'fond-type constructions of the four exponentials subtree.

Preamble

import Mathlib

Formal statement

namespace Transcendence

theorem length_sum_le {ι : Type*} (s : Finset ι) (f : ι → Polynomial (Polynomial ℤ)) :
    ∑ k ∈ (∑ i ∈ s, f i).support, ∑ j ∈ ((∑ i ∈ s, f i).coeff k).support,
        (((∑ i ∈ s, f i).coeff k).coeff j).natAbs ≤
      ∑ i ∈ s, ∑ k ∈ (f i).support, ∑ j ∈ ((f i).coeff k).support, (((f i).coeff k).coeff j).natAbs := by
  sorry

end Transcendence

Source

Standard. Formal proof: Diaz modulus mission, 25 September 2026 (C. Perassi).

View graph