Pythagorean Triples and Fermat’s Fourth-Power Descent — Exact Proof Explorer

The two symmetric Euclidean cross products are exactly twice their natural product.

Euclid's subtraction-free Pythagorean identity follows from the witnessed square difference and the checked Brahmagupta identity.

Every witnessed natural square difference constructs an explicit Euclidean Pythagorean triple.

Swapping the two legs of a natural Pythagorean triple preserves its exact equation.

Euclid's explicit constructor supplies either canonical ordering of its odd/difference and doubled-product legs.

The Euclidean cross-product leg has an exact, explicitly witnessed even half.

The explicitly even Euclidean cross-product coordinate cannot simultaneously have an odd witness.

The natural Euclidean square-difference coordinate is unique without subtraction or classical choice.

Every witnessed natural parameter inequality n≤m produces the exact subtraction-free square-difference witness m²=n²+d.

Every ordered pair of natural Euclidean parameters constructs a witnessed Pythagorean triple without subtraction or a supplied square-difference hypothesis.

A nonzero first Euclidean parameter yields a genuinely nonzero natural hypotenuse.

Natural common-divisor coprimality is symmetric with no gcd choice or excluded middle.

Primitive Pythagorean triples remain primitive after swapping their legs, with coprimality proved by explicit common-divisor witnesses.

A positive fourth-power square counterexample necessarily supplies a Pythagorean triple whose two legs are natural squares.

Ordinary bounded natural induction rejects every positive Fermat-four counterexample once an exact strictly smaller counterexample constructor is supplied.

The stronger no-fourth-powers-sum-to-a-square theorem follows constructively from precisely one explicit, still-unproved strict descent premise.

Fermat's exponent-four equation is impossible if, and only insofar as, the explicitly stated stronger square-hypotenuse strict-descent obligation is proved.

The square of a witnessed even Euclidean parameter has an explicit even half.

The square of a witnessed odd Euclidean parameter has an explicit odd half.

An even first parameter and odd second parameter force their witnessed square difference to be odd.

An odd first parameter and even second parameter force their witnessed square difference to be odd.

Opposite-parity Euclidean parameters force the subtraction-free square-difference leg to be odd in either parity orientation.

The Euclidean hypotenuse is explicitly odd whenever its two parameters have opposite parity.

Every witnessed odd natural is coprime to two, using the actual prime-two theorem and constructive prime nondivisibility.

Every explicitly witnessed divisor of a parameter also divides its natural square.

A square-difference leg is coprime to the first Euclidean parameter whenever the parameters themselves are coprime.

A square-difference leg is coprime to the second Euclidean parameter whenever the parameters themselves are coprime.

A square-difference leg is coprime to the complete Euclidean parameter product.

Coprime opposite-parity Euclidean parameters yield genuinely coprime square-difference and doubled-product legs.

The complete forward primitive Euclid constructor proves both the exact Pythagorean identity and coprimality of its two displayed legs.

Every witnessed ordered pair of coprime opposite-parity natural parameters constructs an actual primitive Euclidean Pythagorean triple.

The complete forward primitive Euclid constructor is valid in either leg orientation.

In every primitive Pythagorean triple, the first leg and hypotenuse have no nonunit common divisor.

In every primitive Pythagorean triple, the second leg and hypotenuse have no nonunit common divisor.

The two legs and hypotenuse of every primitive Pythagorean triple are pairwise coprime constructively.

The two legs of a primitive Pythagorean triple cannot both have even witnesses.

The sum of two witnessed odd squares has exact residue two modulo four.

No natural square is congruent to two modulo four, by uniqueness of bounded constructive remainders.

The two legs of any Pythagorean triple cannot both be odd, independently of primitiveness.

Every natural has a constructive disjunction of explicit even and odd witnesses.

Every primitive Pythagorean triple has genuinely opposite-parity legs with an explicit constructive choice of orientation.

An explicitly odd natural square has an explicitly odd natural root.

Every primitive natural Pythagorean triple has an explicitly witnessed odd hypotenuse.

Every primitive Pythagorean triple admits its complete constructive parity and pairwise-coprimality normal form.

Squaring strictly preserves witnessed order on all natural numbers.

A witnessed weak inequality between natural squares reflects to their roots.

A witnessed strict inequality between natural squares reflects to their roots.

Natural square roots are unique, including zero.

An actual natural square is zero only when its root is zero.

For coprime original factors, reducing a factor and the product root by their gcd exposes the two exact square roots.

If two coprime naturals have square product, each has a constructed natural square root, including both zero boundary cases.

A square divisibility equation between reduced coprime cofactors forces the denominator cofactor to be one.

For all naturals, if a squared divisor divides a squared value, the unsquared divisor divides the unsquared value.

Adding a positive natural gives an explicitly witnessed strict increase.

Each leg of a Pythagorean triangle is strictly below the hypotenuse when the other leg is positive.

The natural difference of ordered odd numbers has a constructive even-half witness.

The sum of an odd leg and its even-shifted hypotenuse is twice the upper half-factor.

The two natural half-factors add exactly to the hypotenuse.

Cancelling the exact square of two proves that the two half-factors multiply to the even-leg half-square.

Every common divisor of the two half-factors divides the original odd leg and hypotenuse, so the factors are coprime.

Coprimality of two natural squares implies coprimality of their explicit roots.

An explicitly even natural square has an explicitly even natural square root.

An odd sum of two squares supplies a constructive choice of opposite parity for their roots.

The roots of the half-factors give the hypotenuse sum and the exact subtraction-free odd-leg gap.

Natural square-root injectivity identifies the even leg with twice the product of the constructed parameters.

The positive odd leg forces the two natural square roots into the required strict Euclidean order.

A positive even leg forces both explicitly constructed Euclidean parameters to be positive.

Every positive-even-leg primitive triangle constructs both coprime half-factors and their actual square-product equation.

Constructive coprime square-factor extraction recovers positive ordered coprime opposite-parity Euclid parameters and every coordinate equation.

Every primitive Pythagorean triangle with positive legs in odd-even order has a fully witnessed Euclidean inverse parametrization.

Swapping positive primitive legs preserves the full exact positive triple definition.

Every positive primitive ordered Pythagorean triple has positive ordered coprime opposite-parity Euclidean parameters in one of both leg orientations.

Strictly ordered parameters with a positive smaller parameter have a positive larger parameter and a positive exact square gap.

The checked Euclidean constructor, strengthened with real positivity, supplies exactly the positive primitive triple used in the classification.

Either canonical Euclidean leg orientation constructs a positive primitive Pythagorean triple with every positivity obligation checked.

Complete constructive classification: a positive ordered triple is primitive Pythagorean if and only if it has positive strictly ordered coprime opposite-parity Euclid parameters in either leg orientation.

The product of two nonzero naturals is nonzero, by the checked zero-product disjunction.

A positive coordinate has a positive square.

Coprime natural bases have coprime squares, with no prime-factorization assumption.

Scaling a fourth power exposes the fourth power of its scale by two explicit product-square identities.

A common scale on the two bases produces an exact fourth-power divisor of the squared hypotenuse.

Cancelling the positive fourth-power scale returns an actual smaller-scale fourth-power counterexample equation.

Adding a nonzero natural strictly increases every natural, with an explicit gap witness.

The square root of the first Euclidean parameter lies strictly below its positive norm, giving the descent measure.

An even square has an explicitly even root, proved by constructive parity cases.

The factor two may pass a natural factor using explicit associativity and commutativity.

A square twice a coprime product with odd first factor supplies an actual square first factor and twice-square second factor.

Every positive fourth-power counterexample constructively reduces to coprime positive bases without increasing the hypotenuse.

The square odd leg in the first parametrization exposes a second primitive Pythagorean triangle on the unsquared base.

The second coprime parameter splitting constructs two positive fourth-power bases with square height strictly below the original norm.

A primitive fourth-power counterexample is an actual primitive triangle with square legs.

Swapping the positive fourth-power bases preserves the primitive counterexample relation.

Two actual primitive Pythagorean inversions and coprime square splittings construct a strictly smaller positive Fermat-four counterexample.

Constructive parity selection orients every primitive counterexample and constructs a strictly smaller counterexample.

Every positive fourth-power square counterexample constructs an actual positive counterexample with strictly smaller height; no descent premise remains.

Unconditional Fermat-four square obstruction follows by the already checked constructive induction theorem and the actual decreasing witness construction.

Fermat's last theorem for exponent four holds unconditionally for every positive natural triple in unchanged Heyting arithmetic.

A nonzero first fourth-power summand forces the square hypotenuse to be nonzero, so its positivity need not be assumed.

Every natural solution of a fourth-power sum equal to a square has a zero summand, including the entire zero boundary.

Fermat exponent four has no nontrivial natural solution, without any separate positivity assumptions.

The complete constructive classification is exact: a fourth-power solution has one zero base and its other base equal to the height, and every such triple is a solution.

Exact campaign G078: the sum of two positive fourth powers is never a square, for every natural z including zero.