Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Sums of four squares are closed under products

Statement

Let m and n be nonnegative integers. If each of m and n is a sum of four integer squares (Representations as sums of four squares), then mn is a sum of four integer squares.

Facts & Assumptions

Given: Nonnegative integers m and n, each a sum of four integer squares.

[F1]

A representation of a nonnegative integer n as a sum of four squares is an ordered quadruple (a,b,c,d)Z4 with n=a2+b2+c2+d2; the integer is a sum of four integer squares when at least one such quadruple exists (Representations as sums of four squares).

[L1]

For all integers x1,,x4,y1,,y4, setting z1=x1y1+x2y2+x3y3+x4y4, z2=x1y2x2y1x3y4+x4y3, z3=x1y3+x2y4x3y1x4y2 and z4=x1y4x2y3+x3y2x4y1 gives (x12+x22+x32+x42)(y12+y22+y32+y42)=z12+z22+z32+z42 (Euler's four-square product identity).

Proof

technique · direct
1.1

Fix quadruples (x1,x2,x3,x4) and (y1,y2,y3,y4) of integers with m=x12+x22+x32+x42 and n=y12+y22+y32+y42, which the hypothesis supplies.

givenF1choose
2.1

With z1,z2,z3,z4 formed from those eight integers by the displayed formulas, mn=(x12+x22+x32+x42)(y12+y22+y32+y42)=z12+z22+z32+z42.

step 1.1L1
3.1

The four integers z1,z2,z3,z4 therefore form a quadruple in Z4 whose squares sum to mn, so mn is a sum of four integer squares; no coordinate is required to be positive or nonzero, so the argument is unaffected when a zi vanishes or is negative, and it covers m=0 and n=0, whose quadruple (0,0,0,0) satisfies the hypothesis and returns z1=z2=z3=z4=0.

step 2.1F1algebra

Remarks

What the identity does and does not give. The four coordinates zi are determined by the two chosen quadruples, so a different choice of representation of m or of n generally produces a different representation of mn. The statement asserts existence only; it makes no claim about how many representations mn has, nor that every representation of mn arises this way.

Why the closure is needed. Reducing Lagrange's four-square theorem: every nonnegative integer is a sum of four integer squares to Every prime is a sum of four integer squares requires exactly this: a factorisation of n into primes is useless unless the property being proved is inherited by products.

Depends on

Used by

Dependency tree · one level

2 results within one dependency step of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources