Attainment of the minimum square sum

Proved

Conway99Formal.CubicMetric.minSquares_attained

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

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

For a finite nonempty set $S$ and integer total $n$ , integer coordinates attain the Euclidean-division bound: $\sum_{i\in S}x_i=n$ and $\sum_{i\in S}x_i^2=\operatorname{minSquares}(|S|,n)$ . Nonemptiness is the only premise.

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_attained {ι : Type*} [DecidableEq ι]
    (s : Finset ι) (total : ℤ) (hs : s.Nonempty) :
    ∃ x : ι → ℤ,
      (∑ i ∈ s, x i) = total ∧
      (∑ i ∈ s, (x i) ^ 2) = minSquares s.card total := by sorry

Source

Exact original Lean source: formalization/2026-10-03/cubic-metric/Arithmetic.lean#74-101; source commit a45708acebe3f397faccb1b646be906f24f23ee5; source SHA-256 cb5b20612f4683979bcf4f2a036ef30d4d5e2d3249e2bddfc63443bdcca909b4. Mechanically extracted declaration: blob/a45708acebe3f397faccb1b646be906f24f23ee5/formalization/2026-10-03/cubic-metric/Arithmetic.lean#L74-L101.

View graph