Fermat and Sums of Two Squares — Exact Proof Explorer

The square of an even natural has an explicit multiple-of-four witness.

The square of an odd natural has an explicit residue-one witness modulo four.

Every natural square is constructively either zero or one modulo four.

A sum of two natural squares has residue zero, one, or two modulo four.

No natural congruent to three modulo four is a sum of two squares.

Every prime congruent to one modulo four has a constructive square root of minus one.

Every prime congruent to one modulo four has a canonical root of minus one strictly below the prime.

A square congruent to the predecessor of a successor yields an explicit divisor of its norm r²+1.

A prime equal to one modulo four divides an explicitly witnessed two-square norm r²+1.

A prime equal to one modulo four divides the norm of a canonical root strictly below the prime.

A positive multiple strictly below twice its divisor must equal that divisor.

A positive two-square norm divisible by p and strictly below 2p is exactly p.

No natural square satisfies the nonunit factor-pair definition of primality.

Witnessed weak order on natural coordinates transports to their squares.

For a prime, its floor-square lower endpoint is strictly smaller than the prime.

Every coordinate at most the floor square root of a prime has square below that prime.

Two natural values each strictly below p have sum strictly below 2p.

Any two coordinates bounded by the prime floor square root have norm strictly below twice the prime.

The successor-floor-square grid has strictly more points than the input modulus.

Every natural admits an explicitly witnessed floor-square grid with more cells than that natural.

A positive divisible norm with floor-square-bounded coordinates is already an exact prime representation.

An explicitly bounded beta-coded map from a larger finite domain cannot be injective.

Every beta-coded prime-residue-bounded map on the oversized floor-square grid has a collision obstruction.

Once collision-versus-injectivity is constructively decided, oversized bounded maps yield an actual collision witness.

A witnessed collision in a finite prefix remains a collision after adjoining one more decoded entry.

If the last decoded value already occurs, its earlier index and final index form an explicit witnessed collision.

An injective decoded prefix stays injective when its new final value has no earlier occurrence.

Every finite beta-coded prefix constructively yields either explicit distinct equal-value indices or a proof of injectivity.

An oversized beta-coded map into a bounded finite interval has an actual existentially witnessed collision.

Every residue-bounded beta map on the floor-square oversized grid contains explicit distinct colliding indices.

Every flat grid index has canonical row, column, affine quotient, and strictly bounded residue witnesses.

Append the next canonical affine residue while preserving every decoded row, column, quotient, and earlier residue.

Every nonzero modulus and positive grid width admit a full beta-coded prefix of bounded affine residues.

The encoded affine residue grid is an explicit BoundedInto map from its full domain into the modulus.

A prime floor-square grid admits a canonical beta-coded affine residue map on all successor-square points.

The actual affine prime-residue grid on all square-root points has explicit distinct flat indices with the same residue.

Equal affine remainders yield an exact subtraction-free balanced congruence between their two grid values.

A balanced congruence to zero yields an actual natural divisibility witness.

Every witnessed natural multiple is balanced-congruent to zero.

Distributivity identifies the scaled negative-one polynomial with the linear square plus its coordinate square.

A witnessed root of minus one forces its scaled linear square plus the coordinate square to vanish modulo the modulus.

Balanced congruence respects squaring of a direct linear relation.

If two naturals sum to zero modulo a modulus, their squares are balanced-congruent without subtraction.

A root of minus one and either matching linear square yield an actual divisible two-square norm.

The same-sign coordinate-difference branch produces a witnessed divisible norm.

The opposite-sign coordinate-difference branch also produces a witnessed divisible norm.

Total natural order supplies an explicit absolute coordinate difference without subtraction.

An absolute difference between two coordinates bounded by s is itself bounded by s.

Every affine collision and both absolute coordinate differences yield exactly one of the constructive same-sign or opposite-sign linear congruences.

An actual balanced affine collision produces explicit natural absolute differences and an actual prime-divisible two-square norm.

A flat index strictly inside a square grid cannot have row index at least the grid width.

Division decoding of a flat index strictly inside a square grid yields a strictly width-bounded row.

A zero witnessed absolute difference forces equality of its source coordinates.

A natural coordinate pair not identically zero has a witnessed strictly positive two-square norm.

Distinct decoded flat indices force strictly positive norm of their witnessed absolute coordinate differences.

A coordinate strictly below S s carries an explicit weak-order witness below s.

Both independently decoded affine remainders equal the same witnessed beta-collision value.

Equal witnessed affine remainders produce an actual balanced affine-congruence certificate.

A genuinely decoded, distinct affine collision at the floor-square grid produces an exact representation of the prime as two natural squares.

Decoding both entries of a genuine beta-coded affine collision yields a complete constructive prime two-square representation.

Every prime congruent to one modulo four has an explicitly witnessed constructive representation as the sum of two natural squares.

Adjacent terms can be constructively exchanged under a shared additive tail.

The square of a natural sum expands into its two squares and two equal cross terms.

A witnessed natural absolute difference satisfies the exact subtraction-free square balance.

The cross products ac·bd and ad·bc coincide by associativity and commutativity.

Distributivity expands a product of two natural two-square norms into four squared products.

The four squared products regroup into diagonal and off-diagonal norm blocks.

The square of a sum separates into its diagonal square block and repeated cross-product block.

Brahmagupta–Fibonacci: the product of two witnessed norms is the norm of ac+bd and the natural magnitude of ad−bc.

Two explicit natural two-square representations compose into an explicit representation of their product.

The zero boundary, multiplicative unit, and exceptional prime two have explicit two-square witnesses.

Every natural square has the direct representation n²+0².

Every prime is constructively either the exceptional prime two or an odd number.

Every prime lies in exactly the constructive residue branches two, one modulo four, or three modulo four.

Scaling a two-square norm by z² scales both coordinates by z.

If a successor divides r²+1, its predecessor is constructively a quadratic residue.

A prime dividing a²+b² but not b supplies an explicit modular root of minus one through the modular inverse of b.

For an odd prime congruent to three modulo four, the first supplementary law excludes square roots of minus one.

A three-modulo-four prime dividing a²+b² must divide the second coordinate, by the constructive first supplementary law.

A prime congruent to three modulo four divides a two-square norm only when it divides both coordinates.

A prime has a natural two-square representation exactly when it is two or congruent to one modulo four.

Associativity and commutativity swap the first two entries of a right-associated natural sum.

Associativity and commutativity swap the first two factors of a right-associated natural product.

The two cross products in the Brahmagupta identity are exactly equal.

The product of two natural two-square norms expands into its four squared coordinate products.

Equal cross products and a witnessed natural difference imply the exact balanced sum-of-two-squares identity.

The nonnegative a*d-b*c branch gives an explicit natural Brahmagupta representation.

The nonnegative b*c-a*d branch gives the same natural Brahmagupta representation.

The product of two two-square norms has the explicit coordinates a*c+b*d and a constructively witnessed absolute difference |a*d-b*c|.

The complete constructive Brahmagupta--Fibonacci identity supplies actual natural coordinates for every product of two-square norms.

Two explicitly represented sums of two natural squares multiply to another explicitly represented sum of two squares.

Restricting a successor-length prefix preserves every witnessed two-square factor representation.

Existentially witnessed represented entries imply representation of every actual decoded value by beta uniqueness.

The final decoded factor of a represented successor prefix has its own explicit two-square witnesses.

Induction on an arbitrary beta-coded product constructs a two-square representation from represented decoded factors.

A represented decoded factor supplied existentially at every bounded index suffices for an explicit representation of the whole product.

The exceptional prime two and every prime congruent to one modulo four have explicit constructive two-square representations.

Every concrete decoded entry in the canonical all-prime prefix is prime, by uniqueness of beta decoding.

Any finite product whose decoded factors are prime two or prime one modulo four is constructively a sum of two squares.

A represented-factor beta product remains constructively representable after multiplication by any explicitly witnessed natural square.

A beta-coded grouped product folds represented prime singletons together with explicit square blocks pairing primes congruent to three modulo four.

Two equal adjacent decoded suffix factors collapse constructively to one explicit square times the shorter beta-coded prefix product.

Appending two equal adjacent decoded factors to any represented beta-coded prefix preserves constructive two-square representability.

A positive natural number all of whose prime divisors are two or one modulo four has an explicitly constructed two-square representation via its canonical prime factorization.

A prime can divide another prime only when both prime values agree.

The prime-power valuation of a distinct prime factor is exactly zero.

The double of a positive natural has an explicit witness for being at least two.

A positive even valuation at a prime yields an actual constructive divisor witness for the prime square.

If a prime square divides a product with one terminal prime factor, that same prime divides the remaining prefix product.

A prime dividing a sorted prime prefix equals its terminal factor whenever that terminal factor is bounded by the prime.

In a sorted all-prime beta factorization, a terminal prime with positive even valuation has the identical immediately preceding factor.

The additive double of a natural equals its standard multiplicative parity witness.

If an additive even block plus a tail is even, the tail has its own constructive additive half witness.

Removing a distinct prime singleton preserves the even valuation of every other prime in a nonzero product.

Removing any nonzero natural-square factor preserves the even valuation of every prime in the remaining cofactor.

A number congruent to three modulo four cannot equal any explicitly represented two-square number.

Removing a represented prime singleton preserves the entire universal three-modulo-four even-valuation invariant.

Removing a nonzero natural-square block preserves every three-modulo-four prime's constructive even-valuation invariant.

The universally quantified bad-prime even-valuation invariant transports constructively along equality of natural values.

The constructive prime residue trichotomy splits into one represented-prime branch and one three-modulo-four branch.

Bounded constructive descent on the natural value proves sufficiency of even valuations at every three-modulo-four prime.

Every nonzero natural whose three-modulo-four prime valuations are all even has an explicitly witnessed two-square representation.

Complete nonzero Fermat two-square classification: witnessed representation is equivalent to even valuation at every three-modulo-four prime.

Full all-natural two-square theorem, with zero explicitly separated from the nonzero even-prime-valuation criterion.

A natural square is zero only when its coordinate is zero.

Zero is an explicit boundary: a two-square norm vanishes exactly when both natural coordinates vanish.

At every prime, the valuation of a nonzero square is exactly twice the valuation of its coordinate.

A common factor of both coordinates extracts as its exact square from their two-square norm.

Two witnessed coordinate divisors provide both quotient coordinates and the exact squared-factor norm identity.

Any common coordinate divisor has its square as an actual divisor of the two-square norm.

Every represented natural remains represented after multiplication by an arbitrary natural square.

A three-modulo-four prime dividing a two-square norm extracts as an exact prime square while preserving a represented quotient.

On the explicit nonzero domain, a three-modulo-four prime square extracts with a nonzero represented quotient.

Multiplying a nonzero value by a nonzero square increases its prime valuation by exactly twice the factor valuation.

A square-factor valuation step preserves constructive evenness of a nonzero quotient's prime valuation.

A positive valuation of a nonzero represented norm at a three-modulo-four prime yields an exact nonzero represented prime-square quotient.

Multiplication of a nonzero natural by a prime square is strictly increasing in witnessed constructive order.

Bounded natural induction proves that a three-modulo-four prime has even valuation in every nonzero represented norm below the bound.

Every three-modulo-four prime has a constructively even valuation in every explicitly nonzero two-square norm.

Necessity direction: every prime congruent to three modulo four has an explicitly even valuation in any represented nonzero natural.