CF0015 · conservative definition

FermatFourStrictDescent

Every positive fourth-power counterexample has a positive counterexample with a strictly smaller natural hypotenuse.

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.

Readable signature

FermatFourStrictDescent()

Exact expansion

forall pff_first_frontier pff_second_frontier pff_hypotenuse_frontier. ((~((pff_first_frontier) = 0) /\ (~((pff_second_frontier) = 0) /\ (~((pff_hypotenuse_frontier) = 0) /\ ((pff_first_frontier) * (pff_first_frontier) * (pff_first_frontier) * (pff_first_frontier) + (pff_second_frontier) * (pff_second_frontier) * (pff_second_frontier) * (pff_second_frontier) = (pff_hypotenuse_frontier) * (pff_hypotenuse_frontier)))))) -> exists pff_smaller_first_frontier pff_smaller_second_frontier pff_smaller_hypotenuse_frontier. (((~((pff_smaller_first_frontier) = 0) /\ (~((pff_smaller_second_frontier) = 0) /\ (~((pff_smaller_hypotenuse_frontier) = 0) /\ ((pff_smaller_first_frontier) * (pff_smaller_first_frontier) * (pff_smaller_first_frontier) * (pff_smaller_first_frontier) + (pff_smaller_second_frontier) * (pff_smaller_second_frontier) * (pff_smaller_second_frontier) * (pff_smaller_second_frontier) = (pff_smaller_hypotenuse_frontier) * (pff_smaller_hypotenuse_frontier)))))) /\ (exists pff_gap_frontier. pff_gap_frontier + S pff_smaller_hypotenuse_frontier = pff_hypotenuse_frontier))

This node is conservative notation, not a theorem, axiom, predicate constant, or kernel rule. Its expansion remains in the unchanged first-order language.

Definition neighborhood

Depends on conservative definitions

CF0014 FermatFourCounterexample PD0002 Lt

Used by conservative definitions

none

All transitive conservative prerequisites

CF0014 FermatFourCounterexample PD0002 Lt

Used by theorem statements or local proof propositions

PF000E fermat_four_bounded_descent PF000F fermat_four_no_square_from_descent PF000G fermat_four_no_fourth_from_descent PF002M fermat_four_strict_descent_proved

Grand-campaign planning vocabulary

Locate FermatFourStrictDescent in the global campaign vocabulary →

Reviewed FermatFourStrictDescent corresponds to blueprint FermatFourStrictDescent with checked argument positions [].

The global atlas describes planning vocabulary and does not itself certify a definition or theorem. The reviewed expansion and conservative dependency DAG on this page are the actual family-local reading definitions.