PF000G · theorem body

fermat_four_no_fourth_from_descent

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Fermat's exponent-four equation is impossible if, and only insofar as, the explicitly stated stronger square-hypotenuse strict-descent obligation is proved.

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.

Statement with defined notation

FermatFourStrictDescent() → ∀ x. ∀ y. ∀ z. ¬x = 0 → ¬y = 0 → ¬z = 0 → ¬x · x · x · x + y · y · y · y = z · z · z · z

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

CF0015 FermatFourStrictDescent

In local proof propositions

CF0014 FermatFourCounterexample
Exact expanded first-order statement
(forall pff_first_bounded pff_second_bounded pff_hypotenuse_bounded. ((~((pff_first_bounded) = 0) /\ (~((pff_second_bounded) = 0) /\ (~((pff_hypotenuse_bounded) = 0) /\ ((pff_first_bounded) * (pff_first_bounded) * (pff_first_bounded) * (pff_first_bounded) + (pff_second_bounded) * (pff_second_bounded) * (pff_second_bounded) * (pff_second_bounded) = (pff_hypotenuse_bounded) * (pff_hypotenuse_bounded)))))) -> exists pff_smaller_first_bounded pff_smaller_second_bounded pff_smaller_hypotenuse_bounded. (((~((pff_smaller_first_bounded) = 0) /\ (~((pff_smaller_second_bounded) = 0) /\ (~((pff_smaller_hypotenuse_bounded) = 0) /\ ((pff_smaller_first_bounded) * (pff_smaller_first_bounded) * (pff_smaller_first_bounded) * (pff_smaller_first_bounded) + (pff_smaller_second_bounded) * (pff_smaller_second_bounded) * (pff_smaller_second_bounded) * (pff_smaller_second_bounded) = (pff_smaller_hypotenuse_bounded) * (pff_smaller_hypotenuse_bounded)))))) /\ (exists pff_gap_bounded. pff_gap_bounded + S pff_smaller_hypotenuse_bounded = pff_hypotenuse_bounded))) -> forall a b h. ~(a = 0) -> ~(b = 0) -> ~(h = 0) -> ~(a * a * a * a + b * b * b * b = h * h * h * h)

Proof neighborhood

Direct theorem prerequisites

PF000F fermat_four_no_square_from_descent fourth_power_regroup · Stable closed mul_eq_zero · Stable closed

Direct theorem dependents

PF002O fermat_four_no_fourth

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

32 script commands · 13 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
fermat four no square from descent
01Fix variables and assumptionsL1–8

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro hstep
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro h
  5. L5
    intro ha
  6. L6
    intro hb
  7. L7
    intro hh
  8. L8
    intro hequation
02Establish hno_squareL9–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply fermat four no square from descent.

  1. L9
    have hno_square : ∀ a. ∀ b. ∀ h. ¬FermatFourCounterexample(a,b,h)Definitions: FermatFourCounterexample(a,b,h)Original native command in the exact edition
  2. L10
    apply fermat_four_no_square_from_descent
  3. L11
    exact hstep
  4. L12
    specialize hno_square a
  5. L13
    specialize hno_square b
  6. L14
    specialize hno_square (h * h)
  7. L15
    apply hno_square
03Separate the logical casesL16–16

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L16
    split
04Use earlier factsL17–17

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L17
    exact ha
05Separate the logical casesL18–18

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L18
    split
06Use earlier factsL19–19

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L19
    exact hb
07Separate the logical casesL20–20

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L20
    split
08Fix variables and assumptionsL21–21

Work with arbitrary variables or the premises of the current implication.

  1. L21
    intro hsquare
09Establish hsplitL22–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul eq zero.

  1. L22
    have hsplit : h = 0 \/ h = 0
  2. L23
    apply mul_eq_zero
  3. L24
    exact hsquare
10Separate the logical casesL25–25

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L25
    cases hsplit
11Use earlier factsL26–30

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L26
    apply hh
  2. L27
    exact hsplit_left
  3. L28
    apply hh
  4. L29
    exact hsplit_right
  5. L30
    specialize fourth_power_regroup h
12Calculate and transport equalitiesL31–31

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L31
    rewrite fourth_power_regroup at hequation
13Use earlier factsL32–32

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L32
    exact hequation

Library-wide reading audit

Original defined command ledger · 32 lines
  1. 0001intro hstep
  2. 0002intro a
  3. 0003intro b
  4. 0004intro h
  5. 0005intro ha
  6. 0006intro hb
  7. 0007intro hh
  8. 0008intro hequation
  9. 0009have hno_square : ∀ a. ∀ b. ∀ h. ¬FermatFourCounterexample(a,b,h)
    Exact native replay linehave hno_square : forall a b h. ~((~((a) = 0) /\ (~((b) = 0) /\ (~((h) = 0) /\ ((a) * (a) * (a) * (a) + (b) * (b) * (b) * (b) = (h) * (h))))))
  10. 0010apply fermat_four_no_square_from_descent
  11. 0011exact hstep
  12. 0012specialize hno_square a
  13. 0013specialize hno_square b
  14. 0014specialize hno_square (h * h)
  15. 0015apply hno_square
  16. 0016split
  17. 0017exact ha
  18. 0018split
  19. 0019exact hb
  20. 0020split
  21. 0021intro hsquare
  22. 0022have hsplit : h = 0 \/ h = 0
  23. 0023apply mul_eq_zero
  24. 0024exact hsquare
  25. 0025cases hsplit
  26. 0026apply hh
  27. 0027exact hsplit_left
  28. 0028apply hh
  29. 0029exact hsplit_right
  30. 0030specialize fourth_power_regroup h
  31. 0031rewrite fourth_power_regroup at hequation
  32. 0032exact hequation