PF000G

fermat_four_no_fourth_from_descent

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

Exact expanded first-order arithmetic 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)

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 32 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

PF000F fermat_four_no_square_from_descent fourth_power_regroup Stable theorem; checked-use authorized mul_eq_zero Stable theorem; checked-use authorized

Direct dependents

PF002O fermat_four_no_fourth

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 : forall a b h. ~((~((a) = 0) /\ (~((b) = 0) /\ (~((h) = 0) /\ ((a) * (a) * (a) * (a) + (b) * (b) * (b) * (b) = (h) * (h))))))
  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 exact 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 : 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