PF002F · theorem body

fermat_four_primitive_normalization

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

Every positive fourth-power counterexample constructively reduces to coprime positive bases without increasing the 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

∀ a. ∀ b. ∀ h. FermatFourCounterexample(a,b,h) → ∃ x. ∃ y. ∃ z. PrimitiveFermatFourCounterexample(x,y,z) ∧ Le(z,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

CF0014 FermatFourCounterexample ND0071 PrimitiveFermatFourCounterexample PD0001 Le

In local proof propositions

PD0003 Dvd PD0005 Coprime PD0006 IsGCD
Exact expanded first-order statement
forall a b h. ((~((a) = 0) /\ (~((b) = 0) /\ (~((h) = 0) /\ ((a) * (a) * (a) * (a) + (b) * (b) * (b) * (b) = (h) * (h)))))) -> exists A B H. (((((~((A) = 0) /\ (~((B) = 0) /\ (~((H) = 0) /\ ((A) * (A) * (A) * (A) + (B) * (B) * (B) * (B) = (H) * (H)))))) /\ (forall pff_divisor_normalize_result. (exists pff_left_normalize_result. (A) = pff_divisor_normalize_result * pff_left_normalize_result) -> (exists pff_right_normalize_result. (B) = pff_divisor_normalize_result * pff_right_normalize_result) -> pff_divisor_normalize_result = 1))) /\ (exists k. k + H = h))

Proof neighborhood

Direct theorem prerequisites

gcd_exists_relational · Stable closed is_gcd_nonzero_coprime_quotients · Alpha closed PF0028 fermat_four_scaled_equation PF001G square_divides_square_root factor_nonzero_right · Alpha closed PF0029 fermat_four_cancel_scaled_equation PF0025 fermat_four_square_nonzero le_scaled_nonzero · Stable closed

Direct theorem dependents

PF002M fermat_four_strict_descent_proved

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

82 script commands · 25 reading checkpoints · 5 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 (4)
fermat four scaled equationsquare divides square rootfermat four cancel scaled equationfermat four square 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 hcounter
02Separate the logical casesL5–7

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

  1. L5
    cases hcounter
  2. L6
    cases hcounter_right
  3. L7
    cases hcounter_right_right
03Establish hgL8–9

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gcd exists relational.

  1. L8
    have hg : ∃ g. IsGCD(g,a,b)Definitions: IsGCD(g,a,b)Original native command in the exact edition
  2. L9
    apply gcd_exists_relational
04Separate the logical casesL10–10

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

  1. L10
    cases hg
05Establish hquotL11–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply is gcd nonzero coprime quotients.

  1. L11
    have hquot : ∃ A. ∃ B. a = x · A ∧ b = x · B ∧ (¬x = 0 ∧ ¬A = 0 ∧ (¬B = 0 ∧ Coprime(A,B)))Definitions: Coprime(A,B)Original native command in the exact edition
  2. L12
    specialize is_gcd_nonzero_coprime_quotients (x)
  3. L13
    specialize is_gcd_nonzero_coprime_quotients (a)
  4. L14
    specialize is_gcd_nonzero_coprime_quotients (b)
  5. L15
    apply is_gcd_nonzero_coprime_quotients
  6. L16
    exact hcounter_left
  7. L17
    exact hcounter_right_left
  8. L18
    exact hg_witness
06Separate the logical casesL19–25

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

  1. L19
    cases hquot
  2. L20
    cases hquot_witness
  3. L21
    cases hquot_witness_witness
  4. L22
    cases hquot_witness_witness_left
  5. L23
    cases hquot_witness_witness_right
  6. L24
    cases hquot_witness_witness_right_left
  7. L25
    cases hquot_witness_witness_right_right
07Establish hscaledL26–35

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

  1. L26
    have hscaled : h * h = ((x * x) * (x * x)) * ((x1 * x1) * (x1 * x1) + (x2 * x2) * (x2 * x2))
  2. L27
    specialize fermat_four_scaled_equation (a)
  3. L28
    specialize fermat_four_scaled_equation (b)
  4. L29
    specialize fermat_four_scaled_equation (h)
  5. L30
    specialize fermat_four_scaled_equation (x)
  6. L31
    specialize fermat_four_scaled_equation (x1)
  7. L32
    specialize fermat_four_scaled_equation (x2)
  8. L33
    apply fermat_four_scaled_equation
  9. L34
    exact hquot_witness_witness_left_left
  10. L35
    exact hquot_witness_witness_left_right
08Use earlier factsL36–36

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

  1. L36
    exact hcounter_right_right_right
09Establish hdivL37–40

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

  1. L37
    have hdiv : Dvd(x · x,h)Definitions: Dvd(x · x,h)Original native command in the exact edition
  2. L38
    specialize square_divides_square_root (x * x)
  3. L39
    specialize square_divides_square_root (h)
  4. L40
    apply square_divides_square_root
10Construct an explicit witnessL41–41

Supply the displayed value, then prove that it has the required property.

  1. L41
    exists (x1 * x1) * (x1 * x1) + (x2 * x2) * (x2 * x2)
11Use earlier factsL42–42

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

  1. L42
    exact hscaled
12Separate the logical casesL43–43

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

  1. L43
    cases hdiv
13Establish hheightL44–52

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

  1. L44
    have hheight : ~(x3 = 0)
  2. L45
    intro hzero
  3. L46
    specialize factor_nonzero_right (h)
  4. L47
    specialize factor_nonzero_right (x * x)
  5. L48
    specialize factor_nonzero_right (x3)
  6. L49
    apply factor_nonzero_right
  7. L50
    exact hcounter_right_right_left
  8. L51
    exact hdiv_witness
  9. L52
    exact hzero
14Construct an explicit witnessL53–55

Supply the displayed value, then prove that it has the required property.

  1. L53
    exists x1
  2. L54
    exists x2
  3. L55
    exists x3
15Separate the logical casesL56–58

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

  1. L56
    split
  2. L57
    split
  3. L58
    split
16Use earlier factsL59–59

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

  1. L59
    exact hquot_witness_witness_right_left_right
17Separate the logical casesL60–60

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

  1. L60
    split
18Use earlier factsL61–61

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

  1. L61
    exact hquot_witness_witness_right_right_left
19Separate the logical casesL62–62

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

  1. L62
    split
20Use earlier factsL63–72

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

  1. L63
    exact hheight
  2. L64
    specialize fermat_four_cancel_scaled_equation (x)
  3. L65
    specialize fermat_four_cancel_scaled_equation (x1)
  4. L66
    specialize fermat_four_cancel_scaled_equation (x2)
  5. L67
    specialize fermat_four_cancel_scaled_equation (x3)
  6. L68
    specialize fermat_four_cancel_scaled_equation (h)
  7. L69
    apply fermat_four_cancel_scaled_equation
  8. L70
    exact hquot_witness_witness_right_left_left
  9. L71
    exact hdiv_witness
  10. L72
    exact hscaled
21Use earlier factsL73–73

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

  1. L73
    exact hquot_witness_witness_right_right_right
22Calculate and transport equalitiesL74–74

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

  1. L74
    rewrite hdiv_witness
23Use earlier factsL75–77

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

  1. L75
    specialize le_scaled_nonzero (x * x)
  2. L76
    specialize le_scaled_nonzero (x3)
  3. L77
    apply le_scaled_nonzero
24Fix variables and assumptionsL78–78

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

  1. L78
    intro hzero
25Use earlier factsL79–82

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

  1. L79
    specialize fermat_four_square_nonzero (x)
  2. L80
    apply fermat_four_square_nonzero
  3. L81
    exact hquot_witness_witness_right_left_left
  4. L82
    exact hzero

Library-wide reading audit

Original defined command ledger · 82 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro h
  4. 0004intro hcounter
  5. 0005cases hcounter
  6. 0006cases hcounter_right
  7. 0007cases hcounter_right_right
  8. 0008have hg : ∃ g. IsGCD(g,a,b)
    Exact native replay linehave hg : exists g. (((exists hag_left_factor_ffd_normalize_gcd. a = g * hag_left_factor_ffd_normalize_gcd) /\ (exists hag_right_factor_ffd_normalize_gcd. b = g * hag_right_factor_ffd_normalize_gcd)) /\ forall hag_divisor_ffd_normalize_gcd. (exists hag_common_left_ffd_normalize_gcd. a = hag_divisor_ffd_normalize_gcd * hag_common_left_ffd_normalize_gcd) -> (exists hag_common_right_ffd_normalize_gcd. b = hag_divisor_ffd_normalize_gcd * hag_common_right_ffd_normalize_gcd) -> exists hag_greatest_factor_ffd_normalize_gcd. g = hag_divisor_ffd_normalize_gcd * hag_greatest_factor_ffd_normalize_gcd)
  9. 0009apply gcd_exists_relational
  10. 0010cases hg
  11. 0011have hquot : ∃ A. ∃ B. a = x · A ∧ b = x · B ∧ (¬x = 0 ∧ ¬A = 0 ∧ (¬B = 0 ∧ Coprime(A,B)))
    Exact native replay linehave hquot : exists A B. ((a = x * A /\ b = x * B) /\ ((~(x = 0) /\ ~(A = 0)) /\ (~(B = 0) /\ (forall pff_divisor_ffd_normalize_quotient. (exists pff_left_ffd_normalize_quotient. (A) = pff_divisor_ffd_normalize_quotient * pff_left_ffd_normalize_quotient) -> (exists pff_right_ffd_normalize_quotient. (B) = pff_divisor_ffd_normalize_quotient * pff_right_ffd_normalize_quotient) -> pff_divisor_ffd_normalize_quotient = 1))))
  12. 0012specialize is_gcd_nonzero_coprime_quotients (x)
  13. 0013specialize is_gcd_nonzero_coprime_quotients (a)
  14. 0014specialize is_gcd_nonzero_coprime_quotients (b)
  15. 0015apply is_gcd_nonzero_coprime_quotients
  16. 0016exact hcounter_left
  17. 0017exact hcounter_right_left
  18. 0018exact hg_witness
  19. 0019cases hquot
  20. 0020cases hquot_witness
  21. 0021cases hquot_witness_witness
  22. 0022cases hquot_witness_witness_left
  23. 0023cases hquot_witness_witness_right
  24. 0024cases hquot_witness_witness_right_left
  25. 0025cases hquot_witness_witness_right_right
  26. 0026have hscaled : h * h = ((x * x) * (x * x)) * ((x1 * x1) * (x1 * x1) + (x2 * x2) * (x2 * x2))
  27. 0027specialize fermat_four_scaled_equation (a)
  28. 0028specialize fermat_four_scaled_equation (b)
  29. 0029specialize fermat_four_scaled_equation (h)
  30. 0030specialize fermat_four_scaled_equation (x)
  31. 0031specialize fermat_four_scaled_equation (x1)
  32. 0032specialize fermat_four_scaled_equation (x2)
  33. 0033apply fermat_four_scaled_equation
  34. 0034exact hquot_witness_witness_left_left
  35. 0035exact hquot_witness_witness_left_right
  36. 0036exact hcounter_right_right_right
  37. 0037have hdiv : Dvd(x · x,h)
    Exact native replay linehave hdiv : exists H. h = (x * x) * H
  38. 0038specialize square_divides_square_root (x * x)
  39. 0039specialize square_divides_square_root (h)
  40. 0040apply square_divides_square_root
  41. 0041exists (x1 * x1) * (x1 * x1) + (x2 * x2) * (x2 * x2)
  42. 0042exact hscaled
  43. 0043cases hdiv
  44. 0044have hheight : ~(x3 = 0)
  45. 0045intro hzero
  46. 0046specialize factor_nonzero_right (h)
  47. 0047specialize factor_nonzero_right (x * x)
  48. 0048specialize factor_nonzero_right (x3)
  49. 0049apply factor_nonzero_right
  50. 0050exact hcounter_right_right_left
  51. 0051exact hdiv_witness
  52. 0052exact hzero
  53. 0053exists x1
  54. 0054exists x2
  55. 0055exists x3
  56. 0056split
  57. 0057split
  58. 0058split
  59. 0059exact hquot_witness_witness_right_left_right
  60. 0060split
  61. 0061exact hquot_witness_witness_right_right_left
  62. 0062split
  63. 0063exact hheight
  64. 0064specialize fermat_four_cancel_scaled_equation (x)
  65. 0065specialize fermat_four_cancel_scaled_equation (x1)
  66. 0066specialize fermat_four_cancel_scaled_equation (x2)
  67. 0067specialize fermat_four_cancel_scaled_equation (x3)
  68. 0068specialize fermat_four_cancel_scaled_equation (h)
  69. 0069apply fermat_four_cancel_scaled_equation
  70. 0070exact hquot_witness_witness_right_left_left
  71. 0071exact hdiv_witness
  72. 0072exact hscaled
  73. 0073exact hquot_witness_witness_right_right_right
  74. 0074rewrite hdiv_witness
  75. 0075specialize le_scaled_nonzero (x * x)
  76. 0076specialize le_scaled_nonzero (x3)
  77. 0077apply le_scaled_nonzero
  78. 0078intro hzero
  79. 0079specialize fermat_four_square_nonzero (x)
  80. 0080apply fermat_four_square_nonzero
  81. 0081exact hquot_witness_witness_right_left_left
  82. 0082exact hzero