Complete constructive universal representation · Constructive arithmetic

Lagrange’s Four-Square Theorem

∀ n ∈ ℕ. ∃ a,b,c,d. n = a² + b² + c² + d²

Explore the complete constructive proof that every natural number is a sum of four squares: both Euler quaternion identities, actual bounded prime seeds, all sixteen signed orientations, strict multiplier descent, and explicit prime-factor witnesses.

Open the definition-aware map Read the final theorem See campaign milestone G064

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Recommended

Defined mathematical notation

Browse 19 linked conservative definitions and 217 theorem bodies without losing their exact first-order expansions.

Browse definitions and theorems →

Focused route

Complete dependency graph

Follow the selected theorem through its constructive prerequisites, linked definitions, and original proof scripts.

Trace prerequisites →

Exact certificate

Fully expanded arithmetic

Inspect 10055 original tactic lines and 717 dependency edges with every definition fully expanded.

Open the exact edition →
Independently verified Alpha v34 checked-use theorem family: 178 displayed closed proofs among 4223 checked release theorems; not Stable: 217 theorem bodies · 19 linked definitions · 10 definition-dependency arrows · 717 proof edges · 10055 tactic lines. dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged.