PF0029 · theorem body

fermat_four_cancel_scaled_equation

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

Cancelling the positive fourth-power scale returns an actual smaller-scale fourth-power counterexample equation.

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 d A B H h. ~(d = 0) -> h = (d * d) * H -> h * h = ((d * d) * (d * d)) * ((A * A) * (A * A) + (B * B) * (B * B)) -> A * A * A * A + B * B * B * B = 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

none

In local proof propositions

CF0011 Pythagorean
Exact expanded first-order statement
forall d A B H h. ~(d = 0) -> h = (d * d) * H -> h * h = ((d * d) * (d * d)) * ((A * A) * (A * A) + (B * B) * (B * B)) -> A * A * A * A + B * B * B * B = H * H

Proof neighborhood

Direct theorem prerequisites

PF0025 fermat_four_square_nonzero four_square_product_square · Alpha closed mul_left_cancel_nonzero · Stable closed fourth_power_regroup · Stable closed

Direct theorem dependents

PF002F fermat_four_primitive_normalization

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

37 script commands · 8 reading checkpoints · 3 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 square nonzero
01Fix variables and assumptionsL1–8

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

  1. L1
    intro d
  2. L2
    intro A
  3. L3
    intro B
  4. L4
    intro H
  5. L5
    intro h
  6. L6
    intro hd
  7. L7
    intro hh
  8. L8
    intro hequation
02Establish hdsquareL9–14

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

  1. L9
    have hdsquare : ~(d * d = 0)
  2. L10
    intro hzero
  3. L11
    specialize fermat_four_square_nonzero (d)
  4. L12
    apply fermat_four_square_nonzero
  5. L13
    exact hd
  6. L14
    exact hzero
03Establish hdfourthL15–20

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

  1. L15
    have hdfourth : ~((d * d) * (d * d) = 0)
  2. L16
    intro hzero
  3. L17
    specialize fermat_four_square_nonzero (d * d)
  4. L18
    apply fermat_four_square_nonzero
  5. L19
    exact hdsquare
  6. L20
    exact hzero
04Establish hnormL21–30

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

  1. L21
    have hnorm : Pythagorean(A · A,B · B,H)Definitions: Pythagorean(A · A,B · B,H)Original native command in the exact edition
  2. L22
    specialize mul_left_cancel_nonzero ((d * d) * (d * d))
  3. L23
    specialize mul_left_cancel_nonzero ((A * A) * (A * A) + (B * B) * (B * B))
  4. L24
    specialize mul_left_cancel_nonzero (H * H)
  5. L25
    apply mul_left_cancel_nonzero
  6. L26
    exact hdfourth
  7. L27
    trans h * h
  8. L28
    symm
  9. L29
    exact hequation
  10. L30
    rewrite hh
05Calculate and transport equalitiesL31–31

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

  1. L31
    rewrite hh
06Use earlier factsL32–32

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

  1. L32
    apply four_square_product_square
07Calculate and transport equalitiesL33–34

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

  1. L33
    trans (A * A) * (A * A) + (B * B) * (B * B)
  2. L34
    congr
08Use earlier factsL35–37

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

  1. L35
    apply fourth_power_regroup
  2. L36
    apply fourth_power_regroup
  3. L37
    exact hnorm

Library-wide reading audit

Original defined command ledger · 37 lines
  1. 0001intro d
  2. 0002intro A
  3. 0003intro B
  4. 0004intro H
  5. 0005intro h
  6. 0006intro hd
  7. 0007intro hh
  8. 0008intro hequation
  9. 0009have hdsquare : ~(d * d = 0)
  10. 0010intro hzero
  11. 0011specialize fermat_four_square_nonzero (d)
  12. 0012apply fermat_four_square_nonzero
  13. 0013exact hd
  14. 0014exact hzero
  15. 0015have hdfourth : ~((d * d) * (d * d) = 0)
  16. 0016intro hzero
  17. 0017specialize fermat_four_square_nonzero (d * d)
  18. 0018apply fermat_four_square_nonzero
  19. 0019exact hdsquare
  20. 0020exact hzero
  21. 0021have hnorm : Pythagorean(A · A,B · B,H)
    Exact native replay linehave hnorm : (A * A) * (A * A) + (B * B) * (B * B) = H * H
  22. 0022specialize mul_left_cancel_nonzero ((d * d) * (d * d))
  23. 0023specialize mul_left_cancel_nonzero ((A * A) * (A * A) + (B * B) * (B * B))
  24. 0024specialize mul_left_cancel_nonzero (H * H)
  25. 0025apply mul_left_cancel_nonzero
  26. 0026exact hdfourth
  27. 0027trans h * h
  28. 0028symm
  29. 0029exact hequation
  30. 0030rewrite hh
  31. 0031rewrite hh
  32. 0032apply four_square_product_square
  33. 0033trans (A * A) * (A * A) + (B * B) * (B * B)
  34. 0034congr
  35. 0035apply fourth_power_regroup
  36. 0036apply fourth_power_regroup
  37. 0037exact hnorm