PF0029

fermat_four_cancel_scaled_equation

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

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

Constructive proof overview

Generated structural guide

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

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

PF0025 fermat_four_square_nonzero four_square_product_square Alpha theorem; checked-use authorized mul_left_cancel_nonzero Stable theorem; checked-use authorized fourth_power_regroup 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

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.

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 : (A * A) * (A * A) + (B * B) * (B * B) = H * H
  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 exact 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 : (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