ND0071 · conservative definition

PrimitiveFermatFourCounterexample

A positive fourth-power counterexample whose two bases are coprime, as constructed by gcd normalization.

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

PrimitiveFermatFourCounterexample(x, y, z)

Exact expansion

(((~((x) = 0) /\ (~((y) = 0) /\ (~((z) = 0) /\ ((x) * (x) * (x) * (x) + (y) * (y) * (y) * (y) = (z) * (z)))))) /\ (forall pff_divisor_firstwave. (exists pff_left_firstwave. (x) = pff_divisor_firstwave * pff_left_firstwave) -> (exists pff_right_firstwave. (y) = pff_divisor_firstwave * pff_right_firstwave) -> pff_divisor_firstwave = 1))

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 PD0005 Coprime

Used by conservative definitions

none

All transitive conservative prerequisites

CF0014 FermatFourCounterexample PD0003 Dvd PD0005 Coprime

Used by theorem statements or local proof propositions

PF002F fermat_four_primitive_normalization PF002I fermat_four_primitive_square_triangle PF002J fermat_four_primitive_counterexample_swap PF002K fermat_four_primitive_odd_even_descent PF002L fermat_four_primitive_descent PF002M fermat_four_strict_descent_proved

Grand-campaign planning vocabulary

Locate PrimitiveFermatFourCounterexample in the global campaign vocabulary →

Reviewed PrimitiveFermatFourCounterexample corresponds to blueprint PrimitiveFermatFourCounterexample 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.