Prime representations and constructive classification · Constructive arithmetic

Fermat and Sums of Two Squares

n = x²+y² ⇔ n = 0 or every p ≡ 3 (mod 4) has even vₚ(n)

Explore the complete constructive all-natural two-square classification: prime representations, multiplication, valuation necessity, strictly decreasing sufficiency, and the explicit zero boundary.

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

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 30 linked conservative definitions and 140 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 4463 original tactic lines and 425 dependency edges with every definition fully expanded.

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