PF002S · theorem body

fermat_four_complete_classification

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

The complete constructive classification is exact: a fourth-power solution has one zero base and its other base equal to the height, and every such triple is a solution.

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

∀ a. ∀ b. ∀ h. (a · a · a · a + b · b · b · b = h · h · h · h → TrivialFermatFourSolution(a,b,h)) ∧ (TrivialFermatFourSolution(a,b,h) → a · a · a · a + b · b · b · b = h · h · h · h)

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

ND0073 TrivialFermatFourSolution

In local proof propositions

none
Exact expanded first-order statement
forall a b h. ((a * a * a * a + b * b * b * b = h * h * h * h -> ((((a) = 0 /\ (b) = (h)) \/ ((b) = 0 /\ (a) = (h))))) /\ (((((a) = 0 /\ (b) = (h)) \/ ((b) = 0 /\ (a) = (h)))) -> a * a * a * a + b * b * b * b = h * h * h * h))

Proof neighborhood

Direct theorem prerequisites

PF002R fermat_four_solutions_have_zero_coordinate PF001B square_eq_injective fourth_power_regroup · Stable closed mul_zero_left · Stable closed zero_add · Stable closed

Direct theorem dependents

none

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

43 script commands · 21 reading checkpoints · 1 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 (2)
fermat four solutions have zero coordinatesquare eq injective
01Fix variables and assumptionsL1–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro h
02Separate the logical casesL4–4

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

  1. L4
    split
03Fix variables and assumptionsL5–5

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

  1. L5
    intro hequation
04Establish hzeroL6–8

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply fermat four solutions have zero coordinate.

  1. L6
    have hzero : a = 0 \/ b = 0
  2. L7
    apply fermat_four_solutions_have_zero_coordinate
  3. L8
    exact hequation
05Separate the logical casesL9–11

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

  1. L9
    cases hzero
  2. L10
    left
  3. L11
    split
06Use earlier factsL12–14

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

  1. L12
    exact hzero_left
  2. L13
    apply square_eq_injective
  3. L14
    apply square_eq_injective
07Calculate and transport equalitiesL15–16

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

  1. L15
    trans b * b * b * b
  2. L16
    symm
08Use earlier factsL17–17

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

  1. L17
    apply fourth_power_regroup
09Calculate and transport equalitiesL18–21

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

  1. L18
    trans h * h * h * h
  2. L19
    trans a * a * a * a + b * b * b * b
  3. L20
    symm
  4. L21
    simp [hzero_left, mul_zero_left, zero_add]
10Use earlier factsL22–23

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

  1. L22
    exact hequation
  2. L23
    apply fourth_power_regroup
11Separate the logical casesL24–25

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

  1. L24
    right
  2. L25
    split
12Use earlier factsL26–28

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

  1. L26
    exact hzero_right
  2. L27
    apply square_eq_injective
  3. L28
    apply square_eq_injective
13Calculate and transport equalitiesL29–30

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

  1. L29
    trans a * a * a * a
  2. L30
    symm
14Use earlier factsL31–31

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

  1. L31
    apply fourth_power_regroup
15Calculate and transport equalitiesL32–35

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

  1. L32
    trans h * h * h * h
  2. L33
    trans a * a * a * a + b * b * b * b
  3. L34
    symm
  4. L35
    simp [hzero_right, mul_zero_left, zero_add]
16Use earlier factsL36–37

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

  1. L36
    exact hequation
  2. L37
    apply fourth_power_regroup
17Fix variables and assumptionsL38–38

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

  1. L38
    intro htrivial
18Separate the logical casesL39–40

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

  1. L39
    cases htrivial
  2. L40
    cases htrivial_left
19Calculate and transport equalitiesL41–41

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

  1. L41
    simp [htrivial_left_left, htrivial_left_right, mul_zero_left, zero_add]
20Separate the logical casesL42–42

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

  1. L42
    cases htrivial_right
21Calculate and transport equalitiesL43–43

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

  1. L43
    simp [htrivial_right_left, htrivial_right_right, mul_zero_left, zero_add]

Library-wide reading audit

Original defined command ledger · 43 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro h
  4. 0004split
  5. 0005intro hequation
  6. 0006have hzero : a = 0 \/ b = 0
  7. 0007apply fermat_four_solutions_have_zero_coordinate
  8. 0008exact hequation
  9. 0009cases hzero
  10. 0010left
  11. 0011split
  12. 0012exact hzero_left
  13. 0013apply square_eq_injective
  14. 0014apply square_eq_injective
  15. 0015trans b * b * b * b
  16. 0016symm
  17. 0017apply fourth_power_regroup
  18. 0018trans h * h * h * h
  19. 0019trans a * a * a * a + b * b * b * b
  20. 0020symm
  21. 0021simp [hzero_left, mul_zero_left, zero_add]
  22. 0022exact hequation
  23. 0023apply fourth_power_regroup
  24. 0024right
  25. 0025split
  26. 0026exact hzero_right
  27. 0027apply square_eq_injective
  28. 0028apply square_eq_injective
  29. 0029trans a * a * a * a
  30. 0030symm
  31. 0031apply fourth_power_regroup
  32. 0032trans h * h * h * h
  33. 0033trans a * a * a * a + b * b * b * b
  34. 0034symm
  35. 0035simp [hzero_right, mul_zero_left, zero_add]
  36. 0036exact hequation
  37. 0037apply fourth_power_regroup
  38. 0038intro htrivial
  39. 0039cases htrivial
  40. 0040cases htrivial_left
  41. 0041simp [htrivial_left_left, htrivial_left_right, mul_zero_left, zero_add]
  42. 0042cases htrivial_right
  43. 0043simp [htrivial_right_left, htrivial_right_right, mul_zero_left, zero_add]