Cornacchia’s sum-of-two-squares algorithm — Exact Proof Explorer

No natural square equals a prime, constructively and without factorization search.

The initial previous remainder p already has square strictly above p.

The square-root stopping test has exactly two constructive branches at a prime: strictly below or strictly above.

Every genuine decreasing Euclidean division has a positive quotient.

Euclidean remainder transport preserves the exact common-divisor coprimality invariant.

Before the square-root threshold, coprime Euclid cannot jump to zero; its next remainder is positive.

The absolute coefficient recurrence preserves positivity without signed natural subtraction.

The next absolute coefficient is an actual natural witness of the multiplication-and-addition recurrence.

The actual remainder and coefficient recurrences preserve p=a*t+r*u exactly.

The cross identity and the previous remainder's square bound force the current positive coefficient's square below p.

Balanced congruence transports an actual natural difference without introducing integer subtraction.

One Euclidean step turns a positive/negative root-coefficient pair into the next positive coefficient congruence.

The other alternating sign branch yields the next opposite coefficient congruence with actual natural witnesses.

Successive actual Euclidean states toggle the two explicit root-coefficient sign patterns.

The actual alternating root invariant makes the current remainder/coefficient two-square norm divisible by p.

At the first positive remainder below sqrt(p), the actual Euclidean coefficient completes an exact two-square representation of p.

A genuine root of minus one modulo a prime is nonzero.

The bounded nonzero root is coprime to its prime, with the bounded-divisibility contradiction checked explicitly.

Every prime one modulo four constructively supplies an actual positive bounded root of minus one for the algorithm.

The initial state (p,root,0,1) has the genuine negative/positive root-coefficient orientation.

A constructed root initializes all arithmetic, coprimality, sign, and threshold invariants of Cornacchia's actual state.

Every actual Euclidean/coefficient transition above the stopping threshold preserves the full rooted invariant and keeps the next remainder positive.

A halted state of the rooted Cornacchia invariant is an exact two-square representation, not just a divisible norm.

A below-threshold positive state is a complete zero-transition Cornacchia run with stored terminal quotient zero.

The actual stopped state can always be encoded in the established beta history without an external coding oracle.

A genuine above-threshold Euclidean division prepends its full remainder/coefficient/quotient state to the same stopped history, preserving every earlier encoded state and transition.

Bounded natural induction on the positive current remainder constructs the entire first-stop history with actual quotients and coefficients and proves its final exact two-square norm.

Every rooted valid Cornacchia state terminates constructively at its first square-root crossing and returns its actual two-square coordinates.

Every positive bounded root of minus one at a prime produces a genuine complete Cornacchia execution and its returned exact representation; no successful trace is supplied.

Full G107: every prime one modulo four yields an actual root of minus one, a complete first-stop Euclidean/coefficient/quotient history from (p,root,0,1), and exactly the two-square representation returned by that history.