Actual Euclidean history · first stopping point · proved representation · Constructive arithmetic

Cornacchia’s sum-of-two-squares algorithm

Prime(p) ∧ p≡1 (mod 4) ⇒ ∃R,T,trace. CornacchiaTrace(p,trace,R,T) ∧ p=R²+T²

Construct the square root of −1, run a genuine finite quotient/remainder trace, and prove that its first square-bounded stopping state represents every prime congruent to one modulo four.

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

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.

Exact certificate

Fully expanded arithmetic

Inspect all 1190 native tactic lines and 112 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem CN001E and follow only the lemmas and conservative definitions supporting cornacchia_prime_two_squares_complete.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G107 milestone → theorem and definition dependencies.
Major independently established statements: CN001E cornacchia_prime_two_squares_complete.
Independently verified Alpha v34 checked-use theorem family: 30 dependency-curried kernel-checked theorem bodies · 112 proof prerequisites · 14 linked definitions · 17 definition-dependency arrows · 1190 exact tactic lines · first admitted v27 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 1224 bundle nodes; SHA-256 c4711433c92b67d2ebeb30131669c60563c70e0464dafa851d417fb88fb21a6d.
Exact mathematical boundary: The output equation is proved from the real first-stop execution; it is not a trace-definition assumption. This is the prime sum-of-two-squares Cornacchia theorem, not a general x²+d y² solver.