CF0014 · conservative definition

FermatFourCounterexample

Three nonzero natural coordinates satisfying the stronger square-hypotenuse counterexample equation x⁴+y⁴=z².

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

FermatFourCounterexample(x, y, z)

Exact expansion

(~((x) = 0) /\ (~((y) = 0) /\ (~((z) = 0) /\ ((x) * (x) * (x) * (x) + (y) * (y) * (y) * (y) = (z) * (z)))))

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

none

Used by conservative definitions

CF0015 FermatFourStrictDescent ND0071 PrimitiveFermatFourCounterexample ND0072 SmallerFermatFourCounterexample

All transitive conservative prerequisites

none

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 PF002F fermat_four_primitive_normalization PF002N fermat_four_no_square

Grand-campaign planning vocabulary

Locate FermatFourCounterexample in the global campaign vocabulary →

Reviewed FermatFourCounterexample corresponds to blueprint FermatFourCounterexample with checked argument positions [0, 1, 2].

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.