PF002H

fermat_four_second_parameter_descent

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

The second coprime parameter splitting constructs two positive fourth-power bases with square height strictly below the original norm.

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 u m n v r s h. ~(u = 0) -> ~(n = 0) -> (forall pff_divisor_ffd_second_parameters. (exists pff_left_ffd_second_parameters. (r) = pff_divisor_ffd_second_parameters * pff_left_ffd_second_parameters) -> (exists pff_right_ffd_second_parameters. (s) = pff_divisor_ffd_second_parameters * pff_right_ffd_second_parameters) -> pff_divisor_ffd_second_parameters = 1) -> m = u * u -> n = 2 * (v * v) -> m = r * r + s * s -> n = 2 * (r * s) -> h = m * m + n * n -> exists A B. ((((~((A) = 0) /\ (~((B) = 0) /\ (~((u) = 0) /\ ((A) * (A) * (A) * (A) + (B) * (B) * (B) * (B) = (u) * (u)))))) /\ (exists ffd_gap_second_result. ffd_gap_second_result + S u = h)))

Constructive proof overview

Generated structural guide

The second coprime parameter splitting constructs two positive fourth-power bases with square height strictly below the original norm.

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

mul_left_cancel_nonzero Stable theorem; checked-use authorized succ_ne_zero Stable theorem; checked-use authorized PF001E coprime_square_product_factors factor_nonzero_left Stable theorem; checked-use authorized factor_nonzero_right Alpha theorem; checked-use authorized fourth_power_regroup Stable theorem; checked-use authorized PF002B fermat_four_root_lt_norm

Direct dependents

PF002K fermat_four_primitive_odd_even_descent

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

117 script commands · 32 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.

Named ingredients (2)
coprime square product factorsfermat four root lt norm
01Fix variables and assumptionsL1–10

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

  1. L1
    intro u
  2. L2
    intro m
  3. L3
    intro n
  4. L4
    intro v
  5. L5
    intro r
  6. L6
    intro s
  7. L7
    intro h
  8. L8
    intro hu
  9. L9
    intro hn
  10. L10
    intro hcoprime
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hm
  2. L12
    intro hnv
  3. L13
    intro hmrs
  4. L14
    intro hnrs
  5. L15
    intro hh
03Establish hproductL16–25

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

  1. L16
    have hproduct : r * s = v * v
  2. L17
    specialize mul_left_cancel_nonzero (2)
  3. L18
    specialize mul_left_cancel_nonzero (r * s)
  4. L19
    specialize mul_left_cancel_nonzero (v * v)
  5. L20
    apply mul_left_cancel_nonzero
  6. L21
    intro hzero
  7. L22
    specialize succ_ne_zero 1
  8. L23
    apply succ_ne_zero
  9. L24
    exact hzero
  10. L25
    trans n
04Calculate and transport equalitiesL26–26

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

  1. L26
    symm
05Use earlier factsL27–28

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

  1. L27
    exact hnrs
  2. L28
    exact hnv
06Establish hsquaresL29–35

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

  1. L29
    have hsquares : exists A B. (r = A * A /\ s = B * B)
  2. L30
    specialize coprime_square_product_factors (r)
  3. L31
    specialize coprime_square_product_factors (s)
  4. L32
    specialize coprime_square_product_factors (v)
  5. L33
    apply coprime_square_product_factors
  6. L34
    exact hcoprime
  7. L35
    exact hproduct
07Separate the logical casesL36–38

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

  1. L36
    cases hsquares
  2. L37
    cases hsquares_witness
  3. L38
    cases hsquares_witness_witness
08Establish hrspositiveL39–47

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

  1. L39
    have hrspositive : ~(r * s = 0)
  2. L40
    intro hzero
  3. L41
    specialize factor_nonzero_right (n)
  4. L42
    specialize factor_nonzero_right (2)
  5. L43
    specialize factor_nonzero_right (r * s)
  6. L44
    apply factor_nonzero_right
  7. L45
    exact hn
  8. L46
    exact hnrs
  9. L47
    exact hzero
09Establish hrL48–56

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

  1. L48
    have hr : ~(r = 0)
  2. L49
    intro hzero
  3. L50
    specialize factor_nonzero_left (r * s)
  4. L51
    specialize factor_nonzero_left (r)
  5. L52
    specialize factor_nonzero_left (s)
  6. L53
    apply factor_nonzero_left
  7. L54
    exact hrspositive
  8. L55
    refl
  9. L56
    exact hzero
10Establish hsL57–65

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

  1. L57
    have hs : ~(s = 0)
  2. L58
    intro hzero
  3. L59
    specialize factor_nonzero_right (r * s)
  4. L60
    specialize factor_nonzero_right (r)
  5. L61
    specialize factor_nonzero_right (s)
  6. L62
    apply factor_nonzero_right
  7. L63
    exact hrspositive
  8. L64
    refl
  9. L65
    exact hzero
11Construct an explicit witnessL66–67

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

  1. L66
    exists x
  2. L67
    exists x1
12Separate the logical casesL68–69

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

  1. L68
    split
  2. L69
    split
13Fix variables and assumptionsL70–70

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

  1. L70
    intro hzero
14Use earlier factsL71–77

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

  1. L71
    specialize factor_nonzero_left (r)
  2. L72
    specialize factor_nonzero_left (x)
  3. L73
    specialize factor_nonzero_left (x)
  4. L74
    apply factor_nonzero_left
  5. L75
    exact hr
  6. L76
    exact hsquares_witness_witness_left
  7. L77
    exact hzero
15Separate the logical casesL78–78

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

  1. L78
    split
16Fix variables and assumptionsL79–79

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

  1. L79
    intro hzero
17Use earlier factsL80–86

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

  1. L80
    specialize factor_nonzero_left (s)
  2. L81
    specialize factor_nonzero_left (x1)
  3. L82
    specialize factor_nonzero_left (x1)
  4. L83
    apply factor_nonzero_left
  5. L84
    exact hs
  6. L85
    exact hsquares_witness_witness_right
  7. L86
    exact hzero
18Separate the logical casesL87–87

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

  1. L87
    split
19Use earlier factsL88–88

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

  1. L88
    exact hu
20Calculate and transport equalitiesL89–90

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

  1. L89
    trans (x * x) * (x * x) + (x1 * x1) * (x1 * x1)
  2. L90
    congr
21Use earlier factsL91–92

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

  1. L91
    apply fourth_power_regroup
  2. L92
    apply fourth_power_regroup
22Calculate and transport equalitiesL93–96

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

  1. L93
    trans r * r + s * s
  2. L94
    congr
  3. L95
    congr
  4. L96
    symm
23Use earlier factsL97–97

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

  1. L97
    exact hsquares_witness_witness_left
24Calculate and transport equalitiesL98–98

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

  1. L98
    symm
25Use earlier factsL99–99

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

  1. L99
    exact hsquares_witness_witness_left
26Calculate and transport equalitiesL100–101

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

  1. L100
    congr
  2. L101
    symm
27Use earlier factsL102–102

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

  1. L102
    exact hsquares_witness_witness_right
28Calculate and transport equalitiesL103–103

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

  1. L103
    symm
29Use earlier factsL104–104

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

  1. L104
    exact hsquares_witness_witness_right
30Calculate and transport equalitiesL105–106

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

  1. L105
    trans m
  2. L106
    symm
31Use earlier factsL107–116

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

  1. L107
    exact hmrs
  2. L108
    exact hm
  3. L109
    specialize fermat_four_root_lt_norm (u)
  4. L110
    specialize fermat_four_root_lt_norm (m)
  5. L111
    specialize fermat_four_root_lt_norm (n)
  6. L112
    specialize fermat_four_root_lt_norm (h)
  7. L113
    apply fermat_four_root_lt_norm
  8. L114
    exact hu
  9. L115
    exact hn
  10. L116
    exact hm
32Use earlier factsL117–117

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

  1. L117
    exact hh

Library-wide reading audit

Original exact command ledger · 117 lines
  1. 0001intro u
  2. 0002intro m
  3. 0003intro n
  4. 0004intro v
  5. 0005intro r
  6. 0006intro s
  7. 0007intro h
  8. 0008intro hu
  9. 0009intro hn
  10. 0010intro hcoprime
  11. 0011intro hm
  12. 0012intro hnv
  13. 0013intro hmrs
  14. 0014intro hnrs
  15. 0015intro hh
  16. 0016have hproduct : r * s = v * v
  17. 0017specialize mul_left_cancel_nonzero (2)
  18. 0018specialize mul_left_cancel_nonzero (r * s)
  19. 0019specialize mul_left_cancel_nonzero (v * v)
  20. 0020apply mul_left_cancel_nonzero
  21. 0021intro hzero
  22. 0022specialize succ_ne_zero 1
  23. 0023apply succ_ne_zero
  24. 0024exact hzero
  25. 0025trans n
  26. 0026symm
  27. 0027exact hnrs
  28. 0028exact hnv
  29. 0029have hsquares : exists A B. (r = A * A /\ s = B * B)
  30. 0030specialize coprime_square_product_factors (r)
  31. 0031specialize coprime_square_product_factors (s)
  32. 0032specialize coprime_square_product_factors (v)
  33. 0033apply coprime_square_product_factors
  34. 0034exact hcoprime
  35. 0035exact hproduct
  36. 0036cases hsquares
  37. 0037cases hsquares_witness
  38. 0038cases hsquares_witness_witness
  39. 0039have hrspositive : ~(r * s = 0)
  40. 0040intro hzero
  41. 0041specialize factor_nonzero_right (n)
  42. 0042specialize factor_nonzero_right (2)
  43. 0043specialize factor_nonzero_right (r * s)
  44. 0044apply factor_nonzero_right
  45. 0045exact hn
  46. 0046exact hnrs
  47. 0047exact hzero
  48. 0048have hr : ~(r = 0)
  49. 0049intro hzero
  50. 0050specialize factor_nonzero_left (r * s)
  51. 0051specialize factor_nonzero_left (r)
  52. 0052specialize factor_nonzero_left (s)
  53. 0053apply factor_nonzero_left
  54. 0054exact hrspositive
  55. 0055refl
  56. 0056exact hzero
  57. 0057have hs : ~(s = 0)
  58. 0058intro hzero
  59. 0059specialize factor_nonzero_right (r * s)
  60. 0060specialize factor_nonzero_right (r)
  61. 0061specialize factor_nonzero_right (s)
  62. 0062apply factor_nonzero_right
  63. 0063exact hrspositive
  64. 0064refl
  65. 0065exact hzero
  66. 0066exists x
  67. 0067exists x1
  68. 0068split
  69. 0069split
  70. 0070intro hzero
  71. 0071specialize factor_nonzero_left (r)
  72. 0072specialize factor_nonzero_left (x)
  73. 0073specialize factor_nonzero_left (x)
  74. 0074apply factor_nonzero_left
  75. 0075exact hr
  76. 0076exact hsquares_witness_witness_left
  77. 0077exact hzero
  78. 0078split
  79. 0079intro hzero
  80. 0080specialize factor_nonzero_left (s)
  81. 0081specialize factor_nonzero_left (x1)
  82. 0082specialize factor_nonzero_left (x1)
  83. 0083apply factor_nonzero_left
  84. 0084exact hs
  85. 0085exact hsquares_witness_witness_right
  86. 0086exact hzero
  87. 0087split
  88. 0088exact hu
  89. 0089trans (x * x) * (x * x) + (x1 * x1) * (x1 * x1)
  90. 0090congr
  91. 0091apply fourth_power_regroup
  92. 0092apply fourth_power_regroup
  93. 0093trans r * r + s * s
  94. 0094congr
  95. 0095congr
  96. 0096symm
  97. 0097exact hsquares_witness_witness_left
  98. 0098symm
  99. 0099exact hsquares_witness_witness_left
  100. 0100congr
  101. 0101symm
  102. 0102exact hsquares_witness_witness_right
  103. 0103symm
  104. 0104exact hsquares_witness_witness_right
  105. 0105trans m
  106. 0106symm
  107. 0107exact hmrs
  108. 0108exact hm
  109. 0109specialize fermat_four_root_lt_norm (u)
  110. 0110specialize fermat_four_root_lt_norm (m)
  111. 0111specialize fermat_four_root_lt_norm (n)
  112. 0112specialize fermat_four_root_lt_norm (h)
  113. 0113apply fermat_four_root_lt_norm
  114. 0114exact hu
  115. 0115exact hn
  116. 0116exact hm
  117. 0117exact hh