Complete primitive classification and unconditional Fermat-four descent · Constructive arithmetic

Pythagorean Triples and Fermat’s Fourth-Power Descent

PrimitiveTriple(a,b,c) ↔ EuclidParametrization(a,b,c) · x,y>0 ⇒ x⁴+y⁴≠z²

Explore both orientations of the complete positive primitive Pythagorean classification, constructive square-factor extraction, and the actual strictly decreasing counterexample construction that proves Fermat’s exponent-four theorem, including every zero-coordinate boundary case.

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

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 102 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 2854 original tactic lines and 322 dependency edges with every definition fully expanded.

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