Lower bound for integer square sums

Proved

Conway99Formal.CubicMetric.minSquares_le_sum_sq

by harry · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

conway99-formal-project-20261003cubic-metricformalized-conditional-result

For finite $S$ and integer coordinates summing to $n$ , $\operatorname{minSquares}(|S|,n)\le\sum_{i\in S}x_i^2$ . The sum condition is explicit; the set may be empty.

Preamble

import Definitions.Def_Arithmetic
import Mathlib

namespace Conway99Formal.CubicMetric
end Conway99Formal.CubicMetric

set_option autoImplicit false

open Conway99Formal.CubicMetric

Formal statement

theorem Conway99Formal.CubicMetric.minSquares_le_sum_sq {ι : Type*} [DecidableEq ι]
    (s : Finset ι) (x : ι → ℤ) (total : ℤ)
    (htotal : ∑ i ∈ s, x i = total) :
    minSquares s.card total ≤ ∑ i ∈ s, (x i) ^ 2 := by sorry

Source

Exact original Lean source: formalization/2026-10-03/cubic-metric/Arithmetic.lean#12-47; source commit a45708acebe3f397faccb1b646be906f24f23ee5; source SHA-256 cb5b20612f4683979bcf4f2a036ef30d4d5e2d3249e2bddfc63443bdcca909b4. Mechanically extracted declaration: blob/a45708acebe3f397faccb1b646be906f24f23ee5/formalization/2026-10-03/cubic-metric/Arithmetic.lean#L12-L47.

View graph