PythagorasNumber.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

7 declarations, 0 contain sorry, 0 declared as axioms

Pythagoras numbers

The Pythagoras number $p(R)$ of $R$ is the least $p$ such that every sum of squares in $R$ is a sum of $p$ squares; see [Pfister1995] for fields and [CDLR1982] for rings. This file defines:

IsSumSqOfLength n a: a is a sum of n squares, a counted refinement of Mathlib's IsSumSq;
pythagorasBounds R: the set of p such that every sum of squares in R is a sum of p squares.

The Pythagoras number of R is p exactly when IsLeast (pythagorasBounds R) p. The set pythagorasBounds R can be empty, in which case the Pythagoras number is infinite; by [CDLR1982] this happens for $\mathbb{R}[X, Y]$. No numeric invariant is defined here, so that no convention for the infinite case is needed.

The definitions and the correspondence with IsSumSq need only [AddCommMonoid R] [Mul R]; the AddCommMonoid is what the sum ∑ i : Fin n requires, since IsSumSq itself assumes only [Mul R] [Add R] [Zero R]. Padding a sum of squares with zeros needs 0 * 0 = 0, so IsSumSqOfLength.of_le and mem_pythagorasBounds_of_le are stated for a NonUnitalNonAssocSemiring.

References

[CDLR1982] M. D. Choi, Z. D. Dai, T. Y. Lam, B. Reznick, The Pythagoras number of some affine algebras and local algebras, J. reine angew. Math. 336 (1982), 45–82.
[Pfister1995] A. Pfister, Quadratic forms with applications to algebraic geometry and topology, London Math. Soc. Lecture Note Ser. 217, Cambridge University Press, 1995.

Imports (2)

Imported by 1 file

FormalConjecturesForMathlib.lean

def IsSumSqOfLength IsSumSqOfLength n a means that a is a sum of n squares line 59 source
Source documentation
IsSumSqOfLength n a means that a is a sum of n squares.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Mul, Nat
Proof uses: Exists, Fin, Eq, Finset.sum, Finset.univ, HMul.hMul
2 instances, coercions and auxiliary constants left out.
```
def IsSumSqOfLength (n : ℕ) (a : R) : Prop :=
…
```
def pythagorasBounds The set of p such that every sum of squares in R is a sum of p squares line 65 source
Source documentation
The set of p such that every sum of squares in R is a sum of p squares. Its least element, when it exists, is the Pythagoras number of R.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Mul, Set, Nat
Proof uses: Set.ofPred, IsSumSq, IsSumSqOfLength
7 instances, coercions and auxiliary constants left out.
```
def pythagorasBounds : Set ℕ :=
…
```
theorem IsSumSqOfLength.isSumSq line 68 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Mul, Nat, IsSumSqOfLength, IsSumSq
Proof uses: Fin, Eq, Finset.sum, Finset.univ, HMul.hMul, Nat.recAux, OfNat.ofNat, of_eq_true, HAdd.hAdd, Eq.mpr, Fin.succ, id, congrArg, Fin.sum_univ_succ, IsSumSq.sq_add, Eq.symm
26 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem IsSumSq.exists_isSumSqOfLength line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Mul, IsSumSq, Exists, Nat, IsSumSqOfLength
Proof uses: IsSumSq.rec, Exists.intro, OfNat.ofNat, Fin, Eq, Finset.sum, Finset.univ, HMul.hMul, of_eq_true, Eq.trans, True, congrArg, HSMul.hSMul, Finset.card, EmptyCollection.emptyCollection, Finset, Finset.sum_congr, Finset.univ_eq_empty, Membership.mem, Eq.refl and 12 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem isSumSq_iff_exists_isSumSqOfLength line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommMonoid, Mul, Iff, IsSumSq, Exists, Nat, IsSumSqOfLength
Proof uses: Iff.intro, IsSumSq.exists_isSumSqOfLength, IsSumSqOfLength.isSumSq
15 instances, coercions and auxiliary constants left out.
theorem IsSumSqOfLength.of_le Padding with zeros: a sum of p squares is a sum of q squares for every q ≥ p line 95 source
Source documentation
Padding with zeros: a sum of p squares is a sum of q squares for every q ≥ p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NonUnitalNonAssocSemiring, Nat, LE.le, IsSumSqOfLength
Proof uses: Fin, Eq, Finset.sum, Finset.univ, HMul.hMul, HAdd.hAdd, Exists, Nat.exists_eq_add_of_le, Exists.intro, Fin.append, OfNat.ofNat, of_eq_true, Eq.trans, True, congrArg, Fin.castAdd, Fin.natAdd, Fin.sum_univ_add, congr, Finset.sum_congr and 10 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem IsSumSqOfLength.of_le {p q : ℕ} (hpq : p ≤ q) {a : R} (h : IsSumSqOfLength p a) :
    IsSumSqOfLength q a := by
…
```
Mentions: IsSumSqOfLength
theorem mem_pythagorasBounds_of_le line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NonUnitalNonAssocSemiring, Nat, LE.le, Membership.mem, Set, pythagorasBounds
Proof uses: IsSumSq, IsSumSqOfLength.of_le
17 instances, coercions and auxiliary constants left out.