PF0028 · theorem body

fermat_four_scaled_equation

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

A common scale on the two bases produces an exact fourth-power divisor of the squared hypotenuse.

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 d A B. a = d * A -> b = d * B -> a * a * a * a + b * b * b * b = h * h -> h * h = ((d * d) * (d * d)) * ((A * A) * (A * A) + (B * B) * (B * B))

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 a b h d A B. a = d * A -> b = d * B -> a * a * a * a + b * b * b * b = h * h -> h * h = ((d * d) * (d * d)) * ((A * A) * (A * A) + (B * B) * (B * B))

Proof neighborhood

Direct theorem prerequisites

PF000D fermat_four_counterexample_is_pythagorean PF0027 fermat_four_scaled_fourth_identity mul_add · 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

34 script commands · 5 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 (2)
fermat four counterexample is pythagoreanfermat four scaled fourth identity
01Fix variables and assumptionsL1–9

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 d
  5. L5
    intro A
  6. L6
    intro B
  7. L7
    intro ha
  8. L8
    intro hb
  9. L9
    intro hequation
02Establish heqL10–19

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

  1. L10
    have heq : Pythagorean(a · a,b · b,h)Definitions: Pythagorean(a · a,b · b,h)Original native command in the exact edition
  2. L11
    specialize fermat_four_counterexample_is_pythagorean (a)
  3. L12
    specialize fermat_four_counterexample_is_pythagorean (b)
  4. L13
    specialize fermat_four_counterexample_is_pythagorean (h)
  5. L14
    apply fermat_four_counterexample_is_pythagorean
  6. L15
    exact hequation
  7. L16
    rewrite ha at heq
  8. L17
    rewrite ha at heq
  9. L18
    rewrite ha at heq
  10. L19
    rewrite ha at heq
03Calculate and transport equalitiesL20–23

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

  1. L20
    rewrite hb at heq
  2. L21
    rewrite hb at heq
  3. L22
    rewrite hb at heq
  4. L23
    rewrite hb at heq
04Establish hAL24–25

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

  1. L24
    have hA : ((d * A) * (d * A)) * ((d * A) * (d * A)) = ((d * d) * (d * d)) * ((A * A) * (A * A))
  2. L25
    apply fermat_four_scaled_fourth_identity
05Establish hBL26–34

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

  1. L26
    have hB : ((d * B) * (d * B)) * ((d * B) * (d * B)) = ((d * d) * (d * d)) * ((B * B) * (B * B))
  2. L27
    apply fermat_four_scaled_fourth_identity
  3. L28
    rewrite hA at heq
  4. L29
    rewrite hB at heq
  5. L30
    trans ((d * d) * (d * d)) * ((A * A) * (A * A)) + ((d * d) * (d * d)) * ((B * B) * (B * B))
  6. L31
    symm
  7. L32
    exact heq
  8. L33
    symm
  9. L34
    apply mul_add

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro h
  4. 0004intro d
  5. 0005intro A
  6. 0006intro B
  7. 0007intro ha
  8. 0008intro hb
  9. 0009intro hequation
  10. 0010have heq : Pythagorean(a · a,b · b,h)
    Exact native replay linehave heq : (a * a) * (a * a) + (b * b) * (b * b) = h * h
  11. 0011specialize fermat_four_counterexample_is_pythagorean (a)
  12. 0012specialize fermat_four_counterexample_is_pythagorean (b)
  13. 0013specialize fermat_four_counterexample_is_pythagorean (h)
  14. 0014apply fermat_four_counterexample_is_pythagorean
  15. 0015exact hequation
  16. 0016rewrite ha at heq
  17. 0017rewrite ha at heq
  18. 0018rewrite ha at heq
  19. 0019rewrite ha at heq
  20. 0020rewrite hb at heq
  21. 0021rewrite hb at heq
  22. 0022rewrite hb at heq
  23. 0023rewrite hb at heq
  24. 0024have hA : ((d * A) * (d * A)) * ((d * A) * (d * A)) = ((d * d) * (d * d)) * ((A * A) * (A * A))
  25. 0025apply fermat_four_scaled_fourth_identity
  26. 0026have hB : ((d * B) * (d * B)) * ((d * B) * (d * B)) = ((d * d) * (d * d)) * ((B * B) * (B * B))
  27. 0027apply fermat_four_scaled_fourth_identity
  28. 0028rewrite hA at heq
  29. 0029rewrite hB at heq
  30. 0030trans ((d * d) * (d * d)) * ((A * A) * (A * A)) + ((d * d) * (d * d)) * ((B * B) * (B * B))
  31. 0031symm
  32. 0032exact heq
  33. 0033symm
  34. 0034apply mul_add