ND0072 · conservative definition

SmallerFermatFourCounterexample

An actual positive fourth-power counterexample together with the explicit strict descent witness z<h.

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

SmallerFermatFourCounterexample(x, y, z, h)

Exact expansion

(((~((x) = 0) /\ (~((y) = 0) /\ (~((z) = 0) /\ ((x) * (x) * (x) * (x) + (y) * (y) * (y) * (y) = (z) * (z)))))) /\ (exists ffd_gap_firstwave. ffd_gap_firstwave + S z = h))

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 PF002H fermat_four_second_parameter_descent PF002K fermat_four_primitive_odd_even_descent PF002L fermat_four_primitive_descent PF002M fermat_four_strict_descent_proved

Grand-campaign planning vocabulary

Locate SmallerFermatFourCounterexample in the global campaign vocabulary →

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

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.