CF0011 · PythagoreanThe exact natural Pythagorean equation, with zero coordinates allowed.
conservative definition · not a theoremCurrent 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.
dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged.
PD0003 · DvdThe natural number d divides n.
conservative definition · not a theoremPD0005 · CoprimeEvery common divisor of a and b is one.
conservative definition · not a theoremPD0009 · Evenn has an even decomposition.
conservative definition · not a theoremPD0010 · Oddn has an odd decomposition.
conservative definition · not a theoremCF0016 · OppositeParityA witnessed choice between even/odd and odd/even parameter orientations.
conservative definition · not a theoremCF0013 · PrimitivePythagoreanThe historical Pythagorean equation with coprime legs; this predicate still permits the zero-leg triples.
conservative definition · not a theoremCF0014 · FermatFourCounterexampleThree nonzero natural coordinates satisfying the stronger square-hypotenuse counterexample equation x⁴+y⁴=z².
conservative definition · not a theoremPD0002 · LtWitness-defined strict order on natural numbers.
conservative definition · not a theoremCF0015 · FermatFourStrictDescentEvery positive fourth-power counterexample has a positive counterexample with a strictly smaller natural hypotenuse.
conservative definition · not a theoremND0069 · PrimitiveTripleExactly the blueprint's positive primitive ordered triple: all three coordinates are nonzero, the square equation holds, and the legs are coprime.
conservative definition · not a theoremND0070 · EuclidParametersExplicit m>n>0, coprime opposite-parity parameters, c=m²+n², the subtraction-free odd-leg equation m²=n²+a, and b=2mn.
conservative definition · not a theoremND0074 · EuclidParametrizationThere exist m>n>0 with coprime opposite-parity parameters and c=m²+n², with either ordered leg orientation (m²−n²,2mn) or (2mn,m²−n²).
conservative definition · not a theoremND0071 · PrimitiveFermatFourCounterexampleA positive fourth-power counterexample whose two bases are coprime, as constructed by gcd normalization.
conservative definition · not a theoremND0072 · SmallerFermatFourCounterexampleAn actual positive fourth-power counterexample together with the explicit strict descent witness z<h.
conservative definition · not a theoremND0073 · TrivialFermatFourSolutionExactly the two zero-coordinate orientations of a natural Fermat-four solution: x=0 and y=z, or y=0 and x=z.
conservative definition · not a theoremPD0001 · LeWitness-defined non-strict order on natural numbers.
conservative definition · not a theoremPD0006 · IsGCDg is a common divisor divisible by every common divisor.
conservative definition · not a theoremPD0011 · Mod4Onen is one modulo four by an explicit quotient.
conservative definition · not a theoremPF0000 · pythagorean_double_productThe two symmetric Euclidean cross products are exactly twice their natural product.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0001 · pythagorean_euclidean_identityEuclid's subtraction-free Pythagorean identity follows from the witnessed square difference and the checked Brahmagupta identity.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0002 · pythagorean_euclidean_constructorEvery witnessed natural square difference constructs an explicit Euclidean Pythagorean triple.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0003 · pythagorean_leg_swapSwapping the two legs of a natural Pythagorean triple preserves its exact equation.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0004 · pythagorean_euclidean_swapped_constructorEuclid's explicit constructor supplies either canonical ordering of its odd/difference and doubled-product legs.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0005 · pythagorean_euclidean_even_legThe Euclidean cross-product leg has an exact, explicitly witnessed even half.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0006 · pythagorean_euclidean_even_leg_not_oddThe explicitly even Euclidean cross-product coordinate cannot simultaneously have an odd witness.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0007 · pythagorean_difference_witness_uniqueThe natural Euclidean square-difference coordinate is unique without subtraction or classical choice.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0008 · pythagorean_square_gap_from_orderEvery witnessed natural parameter inequality n≤m produces the exact subtraction-free square-difference witness m²=n²+d.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0009 · pythagorean_euclidean_from_orderEvery ordered pair of natural Euclidean parameters constructs a witnessed Pythagorean triple without subtraction or a supplied square-difference hypothesis.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000A · pythagorean_hypotenuse_nonzeroA nonzero first Euclidean parameter yields a genuinely nonzero natural hypotenuse.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000B · pythagorean_coprime_swapNatural common-divisor coprimality is symmetric with no gcd choice or excluded middle.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000C · pythagorean_primitive_leg_swapPrimitive Pythagorean triples remain primitive after swapping their legs, with coprimality proved by explicit common-divisor witnesses.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000D · fermat_four_counterexample_is_pythagoreanA positive fourth-power square counterexample necessarily supplies a Pythagorean triple whose two legs are natural squares.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000E · fermat_four_bounded_descentOrdinary bounded natural induction rejects every positive Fermat-four counterexample once an exact strictly smaller counterexample constructor is supplied.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000F · fermat_four_no_square_from_descentThe stronger no-fourth-powers-sum-to-a-square theorem follows constructively from precisely one explicit, still-unproved strict descent premise.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000G · fermat_four_no_fourth_from_descentFermat's exponent-four equation is impossible if, and only insofar as, the explicitly stated stronger square-hypotenuse strict-descent obligation is proved.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000H · pythagorean_parameter_even_squareThe square of a witnessed even Euclidean parameter has an explicit even half.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000I · pythagorean_parameter_odd_squareThe square of a witnessed odd Euclidean parameter has an explicit odd half.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000J · pythagorean_even_odd_square_gap_oddAn even first parameter and odd second parameter force their witnessed square difference to be odd.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000K · pythagorean_odd_even_square_gap_oddAn odd first parameter and even second parameter force their witnessed square difference to be odd.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000L · pythagorean_opposite_parity_square_gap_oddOpposite-parity Euclidean parameters force the subtraction-free square-difference leg to be odd in either parity orientation.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000M · pythagorean_opposite_parity_hypotenuse_oddThe Euclidean hypotenuse is explicitly odd whenever its two parameters have opposite parity.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000N · pythagorean_odd_coordinate_coprime_twoEvery witnessed odd natural is coprime to two, using the actual prime-two theorem and constructive prime nondivisibility.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000O · pythagorean_parameter_divisor_divides_squareEvery explicitly witnessed divisor of a parameter also divides its natural square.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000P · pythagorean_square_gap_coprime_first_parameterA square-difference leg is coprime to the first Euclidean parameter whenever the parameters themselves are coprime.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000Q · pythagorean_square_gap_coprime_second_parameterA square-difference leg is coprime to the second Euclidean parameter whenever the parameters themselves are coprime.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000R · pythagorean_square_gap_coprime_parameter_productA square-difference leg is coprime to the complete Euclidean parameter product.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000S · pythagorean_primitive_euclidean_legsCoprime opposite-parity Euclidean parameters yield genuinely coprime square-difference and doubled-product legs.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000T · pythagorean_primitive_euclidean_constructorThe complete forward primitive Euclid constructor proves both the exact Pythagorean identity and coprimality of its two displayed legs.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000U · pythagorean_primitive_euclidean_from_orderEvery witnessed ordered pair of coprime opposite-parity natural parameters constructs an actual primitive Euclidean Pythagorean triple.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000V · pythagorean_primitive_euclidean_swapped_constructorThe complete forward primitive Euclid constructor is valid in either leg orientation.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000W · pythagorean_primitive_hypotenuse_coprime_first_legIn every primitive Pythagorean triple, the first leg and hypotenuse have no nonunit common divisor.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000X · pythagorean_primitive_hypotenuse_coprime_second_legIn every primitive Pythagorean triple, the second leg and hypotenuse have no nonunit common divisor.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000Y · pythagorean_primitive_pairwise_coprimeThe two legs and hypotenuse of every primitive Pythagorean triple are pairwise coprime constructively.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF000Z · pythagorean_primitive_legs_not_both_evenThe two legs of a primitive Pythagorean triple cannot both have even witnesses.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0010 · pythagorean_odd_square_pair_two_mod_fourThe sum of two witnessed odd squares has exact residue two modulo four.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0011 · pythagorean_two_mod_four_not_squareNo natural square is congruent to two modulo four, by uniqueness of bounded constructive remainders.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0012 · pythagorean_triple_legs_not_both_oddThe two legs of any Pythagorean triple cannot both be odd, independently of primitiveness.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0013 · pythagorean_coordinate_parity_choiceEvery natural has a constructive disjunction of explicit even and odd witnesses.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0014 · pythagorean_primitive_legs_opposite_parityEvery primitive Pythagorean triple has genuinely opposite-parity legs with an explicit constructive choice of orientation.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0015 · pythagorean_odd_square_has_odd_rootAn explicitly odd natural square has an explicitly odd natural root.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0016 · pythagorean_primitive_hypotenuse_oddEvery primitive natural Pythagorean triple has an explicitly witnessed odd hypotenuse.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0017 · pythagorean_primitive_normal_formEvery primitive Pythagorean triple admits its complete constructive parity and pairwise-coprimality normal form.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0018 · square_lt_strictSquaring strictly preserves witnessed order on all natural numbers.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0019 · square_le_reflectA witnessed weak inequality between natural squares reflects to their roots.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001A · square_lt_reflectA witnessed strict inequality between natural squares reflects to their roots.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001B · square_eq_injectiveNatural square roots are unique, including zero.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001C · square_zero_rootAn actual natural square is zero only when its root is zero.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001D · coprime_square_reduced_factorsFor coprime original factors, reducing a factor and the product root by their gcd exposes the two exact square roots.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001E · coprime_square_product_factorsIf two coprime naturals have square product, each has a constructed natural square root, including both zero boundary cases.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001F · square_divides_square_reduced_rootA square divisibility equation between reduced coprime cofactors forces the denominator cofactor to be one.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001G · square_divides_square_rootFor all naturals, if a squared divisor divides a squared value, the unsquared divisor divides the unsquared value.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001H · pythagorean_positive_add_strictAdding a positive natural gives an explicitly witnessed strict increase.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001I · pythagorean_leg_strictly_below_hypotenuseEach leg of a Pythagorean triangle is strictly below the hypotenuse when the other leg is positive.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001J · pythagorean_odd_ordered_difference_evenThe natural difference of ordered odd numbers has a constructive even-half witness.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001K · pythagorean_half_sum_reassociationThe sum of an odd leg and its even-shifted hypotenuse is twice the upper half-factor.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001L · pythagorean_half_hypotenuse_reassociationThe two natural half-factors add exactly to the hypotenuse.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001M · pythagorean_half_product_is_squareCancelling the exact square of two proves that the two half-factors multiply to the even-leg half-square.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001N · pythagorean_half_factors_coprimeEvery common divisor of the two half-factors divides the original odd leg and hypotenuse, so the factors are coprime.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001O · pythagorean_coprime_square_rootsCoprimality of two natural squares implies coprimality of their explicit roots.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001P · pythagorean_even_square_has_even_rootAn explicitly even natural square has an explicitly even natural square root.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001Q · pythagorean_odd_square_sum_opposite_rootsAn odd sum of two squares supplies a constructive choice of opposite parity for their roots.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001R · pythagorean_half_roots_coordinatesThe roots of the half-factors give the hypotenuse sum and the exact subtraction-free odd-leg gap.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001S · pythagorean_half_roots_even_legNatural square-root injectivity identifies the even leg with twice the product of the constructed parameters.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001T · pythagorean_positive_gap_orders_parametersThe positive odd leg forces the two natural square roots into the required strict Euclidean order.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001U · pythagorean_positive_even_leg_parameters_nonzeroA positive even leg forces both explicitly constructed Euclidean parameters to be positive.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001V · pythagorean_odd_even_half_factorsEvery positive-even-leg primitive triangle constructs both coprime half-factors and their actual square-product equation.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001W · pythagorean_half_factors_extract_parametersConstructive coprime square-factor extraction recovers positive ordered coprime opposite-parity Euclid parameters and every coordinate equation.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001X · pythagorean_primitive_odd_even_inverseEvery primitive Pythagorean triangle with positive legs in odd-even order has a fully witnessed Euclidean inverse parametrization.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001Y · pythagorean_positive_primitive_leg_swapSwapping positive primitive legs preserves the full exact positive triple definition.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF001Z · pythagorean_positive_primitive_inverseEvery positive primitive ordered Pythagorean triple has positive ordered coprime opposite-parity Euclidean parameters in one of both leg orientations.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0020 · pythagorean_ordered_gap_positiveStrictly ordered parameters with a positive smaller parameter have a positive larger parameter and a positive exact square gap.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0021 · pythagorean_euclidean_parameters_positive_constructorThe checked Euclidean constructor, strengthened with real positivity, supplies exactly the positive primitive triple used in the classification.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0022 · pythagorean_positive_primitive_from_parametersEither canonical Euclidean leg orientation constructs a positive primitive Pythagorean triple with every positivity obligation checked.
theorem body · 6 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0023 · pythagorean_positive_primitive_classificationComplete 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.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0024 · fermat_four_product_nonzeroThe product of two nonzero naturals is nonzero, by the checked zero-product disjunction.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0025 · fermat_four_square_nonzeroA positive coordinate has a positive square.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0026 · fermat_four_coprime_squaresCoprime natural bases have coprime squares, with no prime-factorization assumption.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0027 · fermat_four_scaled_fourth_identityScaling a fourth power exposes the fourth power of its scale by two explicit product-square identities.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0028 · fermat_four_scaled_equationA common scale on the two bases produces an exact fourth-power divisor of the squared hypotenuse.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF0029 · fermat_four_cancel_scaled_equationCancelling the positive fourth-power scale returns an actual smaller-scale fourth-power counterexample equation.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002A · fermat_four_lt_add_positiveAdding a nonzero natural strictly increases every natural, with an explicit gap witness.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002B · fermat_four_root_lt_normThe square root of the first Euclidean parameter lies strictly below its positive norm, giving the descent measure.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002C · fermat_four_even_square_rootAn even square has an explicitly even root, proved by constructive parity cases.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002D · fermat_four_double_product_commuteThe factor two may pass a natural factor using explicit associativity and commutativity.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002E · fermat_four_odd_double_square_factorsA square twice a coprime product with odd first factor supplies an actual square first factor and twice-square second factor.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002F · fermat_four_primitive_normalizationEvery positive fourth-power counterexample constructively reduces to coprime positive bases without increasing the hypotenuse.
theorem body · 6 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002G · fermat_four_nested_primitive_triangleThe square odd leg in the first parametrization exposes a second primitive Pythagorean triangle on the unsquared base.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002H · fermat_four_second_parameter_descentThe second coprime parameter splitting constructs two positive fourth-power bases with square height strictly below the original norm.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002I · fermat_four_primitive_square_triangleA primitive fourth-power counterexample is an actual primitive triangle with square legs.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002J · fermat_four_primitive_counterexample_swapSwapping the positive fourth-power bases preserves the primitive counterexample relation.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002K · fermat_four_primitive_odd_even_descentTwo actual primitive Pythagorean inversions and coprime square splittings construct a strictly smaller positive Fermat-four counterexample.
theorem body · 6 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002L · fermat_four_primitive_descentConstructive parity selection orients every primitive counterexample and constructs a strictly smaller counterexample.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002M · fermat_four_strict_descent_provedEvery positive fourth-power square counterexample constructs an actual positive counterexample with strictly smaller height; no descent premise remains.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002N · fermat_four_no_squareUnconditional Fermat-four square obstruction follows by the already checked constructive induction theorem and the actual decreasing witness construction.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002O · fermat_four_no_fourthFermat's last theorem for exponent four holds unconditionally for every positive natural triple in unchanged Heyting arithmetic.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002P · fermat_four_equation_height_nonzeroA nonzero first fourth-power summand forces the square hypotenuse to be nonzero, so its positivity need not be assumed.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002Q · fermat_four_square_solutions_have_zero_coordinateEvery natural solution of a fourth-power sum equal to a square has a zero summand, including the entire zero boundary.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002R · fermat_four_solutions_have_zero_coordinateFermat exponent four has no nontrivial natural solution, without any separate positivity assumptions.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002S · fermat_four_complete_classificationThe 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.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StablePF002T · fermat_four_positive_sum_not_squareExact campaign G078: the sum of two positive fourth powers is never a square, for every natural z including zero.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not Stable