PF002Q · theorem body

fermat_four_square_solutions_have_zero_coordinate

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

Every natural solution of a fourth-power sum equal to a square has a zero summand, including the entire zero boundary.

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

forall a b h. a * a * a * a + b * b * b * b = h * h -> (a = 0 \/ b = 0)

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

none

In local proof propositions

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

Proof neighborhood

Direct theorem prerequisites

eq_decidable · Stable closed PF002N fermat_four_no_square PF002P fermat_four_equation_height_nonzero

Direct theorem dependents

PF002R fermat_four_solutions_have_zero_coordinate PF002T fermat_four_positive_sum_not_square

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

33 script commands · 16 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 (2)
fermat four no squarefermat four equation height nonzero
01Fix variables and assumptionsL1–4

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro h
  4. L4
    intro hequation
02Establish hacasesL5–6

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

  1. L5
    have hacases : a = 0 \/ ~(a = 0)
  2. L6
    apply eq_decidable
03Separate the logical casesL7–8

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

  1. L7
    cases hacases
  2. L8
    left
04Use earlier factsL9–9

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

  1. L9
    exact hacases_left
05Establish hbcasesL10–11

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

  1. L10
    have hbcases : b = 0 \/ ~(b = 0)
  2. L11
    apply eq_decidable
06Separate the logical casesL12–13

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

  1. L12
    cases hbcases
  2. L13
    right
07Use earlier factsL14–14

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

  1. L14
    exact hbcases_left
08Separate the logical casesL15–15

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

  1. L15
    exfalso
09Use earlier factsL16–19

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

  1. L16
    specialize fermat_four_no_square (a)
  2. L17
    specialize fermat_four_no_square (b)
  3. L18
    specialize fermat_four_no_square (h)
  4. L19
    apply fermat_four_no_square
10Separate the logical casesL20–20

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

  1. L20
    split
11Use earlier factsL21–21

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

  1. L21
    exact hacases_right
12Separate the logical casesL22–22

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

  1. L22
    split
13Use earlier factsL23–23

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

  1. L23
    exact hbcases_right
14Separate the logical casesL24–24

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

  1. L24
    split
15Fix variables and assumptionsL25–25

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

  1. L25
    intro hzero
16Use earlier factsL26–33

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

  1. L26
    specialize fermat_four_equation_height_nonzero (a)
  2. L27
    specialize fermat_four_equation_height_nonzero (b)
  3. L28
    specialize fermat_four_equation_height_nonzero (h)
  4. L29
    apply fermat_four_equation_height_nonzero
  5. L30
    exact hacases_right
  6. L31
    exact hequation
  7. L32
    exact hzero
  8. L33
    exact hequation

Library-wide reading audit

Original defined command ledger · 33 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro h
  4. 0004intro hequation
  5. 0005have hacases : a = 0 \/ ~(a = 0)
  6. 0006apply eq_decidable
  7. 0007cases hacases
  8. 0008left
  9. 0009exact hacases_left
  10. 0010have hbcases : b = 0 \/ ~(b = 0)
  11. 0011apply eq_decidable
  12. 0012cases hbcases
  13. 0013right
  14. 0014exact hbcases_left
  15. 0015exfalso
  16. 0016specialize fermat_four_no_square (a)
  17. 0017specialize fermat_four_no_square (b)
  18. 0018specialize fermat_four_no_square (h)
  19. 0019apply fermat_four_no_square
  20. 0020split
  21. 0021exact hacases_right
  22. 0022split
  23. 0023exact hbcases_right
  24. 0024split
  25. 0025intro hzero
  26. 0026specialize fermat_four_equation_height_nonzero (a)
  27. 0027specialize fermat_four_equation_height_nonzero (b)
  28. 0028specialize fermat_four_equation_height_nonzero (h)
  29. 0029apply fermat_four_equation_height_nonzero
  30. 0030exact hacases_right
  31. 0031exact hequation
  32. 0032exact hzero
  33. 0033exact hequation