PF0028

fermat_four_scaled_equation

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 34 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

PF000D fermat_four_counterexample_is_pythagorean PF0027 fermat_four_scaled_fourth_identity mul_add Stable theorem; checked-use authorized

Direct dependents

PF002F fermat_four_primitive_normalization

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

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.

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 : (a * a) * (a * a) + (b * b) * (b * b) = h * h
  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 exact 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 : (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