PF001D

coprime_square_reduced_factors

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

For coprime original factors, reducing a factor and the product root by their gcd exposes the two exact square roots.

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 z g A Z. ~(g = 0) -> ~(Z = 0) -> a = g * A -> z = g * Z -> a * b = z * z -> (forall frp_divisor_csf_reduced_original. (exists frp_left_factor_csf_reduced_original. a = frp_divisor_csf_reduced_original * frp_left_factor_csf_reduced_original) -> (exists frp_right_factor_csf_reduced_original. b = frp_divisor_csf_reduced_original * frp_right_factor_csf_reduced_original) -> frp_divisor_csf_reduced_original = 1) -> (forall frp_divisor_csf_reduced_quotients. (exists frp_left_factor_csf_reduced_quotients. A = frp_divisor_csf_reduced_quotients * frp_left_factor_csf_reduced_quotients) -> (exists frp_right_factor_csf_reduced_quotients. Z = frp_divisor_csf_reduced_quotients * frp_right_factor_csf_reduced_quotients) -> frp_divisor_csf_reduced_quotients = 1) -> a = A * A /\ b = Z * Z

Constructive proof overview

Generated structural guide

For coprime original factors, reducing a factor and the product root by their gcd exposes the two exact square roots.

The unchanged tactic script uses 11 declared prerequisites and contains 98 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 mul_right_cancel_nonzero Stable theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized four_square_product_square Alpha theorem; checked-use authorized four_square_descent_nonzero_square Alpha theorem; checked-use authorized coprime_symm Stable theorem; checked-use authorized coprime_mul_left Stable theorem; checked-use authorized gauss_coprime_cancel Stable theorem; checked-use authorized mul_one Stable theorem; checked-use authorized one_mul Stable theorem; checked-use authorized

Direct dependents

PF001E coprime_square_product_factors

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

98 script commands · 31 reading checkpoints · 7 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro z
  4. L4
    intro g
  5. L5
    intro A
  6. L6
    intro Z
  7. L7
    intro hg
  8. L8
    intro hZ
  9. L9
    intro ha
  10. L10
    intro hz
02Fix variables and assumptionsL11–13

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

  1. L11
    intro heq
  2. L12
    intro hab
  3. L13
    intro hAZ
03Establish hreducedL14–23

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

  1. L14
    have hreduced : A * b = g * (Z * Z)
  2. L15
    specialize mul_left_cancel_nonzero g
  3. L16
    specialize mul_left_cancel_nonzero (A * b)
  4. L17
    specialize mul_left_cancel_nonzero (g * (Z * Z))
  5. L18
    apply mul_left_cancel_nonzero
  6. L19
    exact hg
  7. L20
    trans a * b
  8. L21
    rewrite ha
  9. L22
    symm
  10. L23
    apply mul_assoc
04Calculate and transport equalitiesL24–24

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

  1. L24
    trans z * z
05Use earlier factsL25–25

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

  1. L25
    exact heq
06Calculate and transport equalitiesL26–28

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

  1. L26
    rewrite hz
  2. L27
    rewrite hz
  3. L28
    trans (g * g) * (Z * Z)
07Use earlier factsL29–30

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

  1. L29
    apply four_square_product_square
  2. L30
    apply mul_assoc
08Establish hZAL31–35

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

  1. L31
    have hZA : forall frp_divisor_csf_reduced_swapped. (exists frp_left_factor_csf_reduced_swapped. Z = frp_divisor_csf_reduced_swapped * frp_left_factor_csf_reduced_swapped) -> (exists frp_right_factor_csf_reduced_swapped. A = frp_divisor_csf_reduced_swapped * frp_right_factor_csf_reduced_swapped) -> frp_divisor_csf_reduced_swapped = 1
  2. L32
    specialize coprime_symm A
  3. L33
    specialize coprime_symm Z
  4. L34
    apply coprime_symm
  5. L35
    exact hAZ
09Establish hZsquareAL36–42

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

  1. L36
    have hZsquareA : forall d. (exists x. Z * Z = d * x) -> (exists y. A = d * y) -> d = 1
  2. L37
    specialize coprime_mul_left Z
  3. L38
    specialize coprime_mul_left Z
  4. L39
    specialize coprime_mul_left A
  5. L40
    apply coprime_mul_left
  6. L41
    exact hZA
  7. L42
    exact hZA
10Establish hbquotL43–48

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

  1. L43
    have hbquot : exists k. b = (Z * Z) * k
  2. L44
    specialize gauss_coprime_cancel (Z * Z)
  3. L45
    specialize gauss_coprime_cancel A
  4. L46
    specialize gauss_coprime_cancel b
  5. L47
    apply gauss_coprime_cancel
  6. L48
    exact hZsquareA
11Construct an explicit witnessL49–49

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

  1. L49
    exists g
12Calculate and transport equalitiesL50–50

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

  1. L50
    trans g * (Z * Z)
13Use earlier factsL51–52

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

  1. L51
    exact hreduced
  2. L52
    apply mul_comm
14Separate the logical casesL53–53

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

  1. L53
    cases hbquot
15Establish hscaleL54–63

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

  1. L54
    have hscale : A * x = g
  2. L55
    specialize mul_right_cancel_nonzero (A * x)
  3. L56
    specialize mul_right_cancel_nonzero g
  4. L57
    specialize mul_right_cancel_nonzero (Z * Z)
  5. L58
    apply mul_right_cancel_nonzero
  6. L59
    intro hzero
  7. L60
    specialize four_square_descent_nonzero_square Z
  8. L61
    apply four_square_descent_nonzero_square
  9. L62
    exact hZ
  10. L63
    exact hzero
16Calculate and transport equalitiesL64–66

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

  1. L64
    trans A * b
  2. L65
    rewrite hbquot_witness
  3. L66
    trans A * (x * (Z * Z))
17Use earlier factsL67–67

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

  1. L67
    apply mul_assoc
18Calculate and transport equalitiesL68–69

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

  1. L68
    congr
  2. L69
    refl
19Use earlier factsL70–71

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

  1. L70
    apply mul_comm
  2. L71
    exact hreduced
20Establish haquotL72–80

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

  1. L72
    have haquot : a = x * (A * A)
  2. L73
    trans g * A
  3. L74
    exact ha
  4. L75
    rewrite <- hscale
  5. L76
    trans (x * A) * A
  6. L77
    congr
  7. L78
    apply mul_comm
  8. L79
    refl
  9. L80
    apply mul_assoc
21Establish hxoneL81–83

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

  1. L81
    have hxone : x = 1
  2. L82
    specialize hab x
  3. L83
    apply hab
22Construct an explicit witnessL84–84

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

  1. L84
    exists (A * A)
23Use earlier factsL85–85

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

  1. L85
    exact haquot
24Construct an explicit witnessL86–86

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

  1. L86
    exists (Z * Z)
25Calculate and transport equalitiesL87–87

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

  1. L87
    trans (Z * Z) * x
26Use earlier factsL88–89

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

  1. L88
    exact hbquot_witness
  2. L89
    apply mul_comm
27Separate the logical casesL90–90

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

  1. L90
    split
28Calculate and transport equalitiesL91–92

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

  1. L91
    rewrite hxone at haquot
  2. L92
    trans 1 * (A * A)
29Use earlier factsL93–94

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

  1. L93
    exact haquot
  2. L94
    apply one_mul
30Calculate and transport equalitiesL95–96

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

  1. L95
    rewrite hxone at hbquot_witness
  2. L96
    trans (Z * Z) * 1
31Use earlier factsL97–98

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

  1. L97
    exact hbquot_witness
  2. L98
    apply mul_one

Library-wide reading audit

Original exact command ledger · 98 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro z
  4. 0004intro g
  5. 0005intro A
  6. 0006intro Z
  7. 0007intro hg
  8. 0008intro hZ
  9. 0009intro ha
  10. 0010intro hz
  11. 0011intro heq
  12. 0012intro hab
  13. 0013intro hAZ
  14. 0014have hreduced : A * b = g * (Z * Z)
  15. 0015specialize mul_left_cancel_nonzero g
  16. 0016specialize mul_left_cancel_nonzero (A * b)
  17. 0017specialize mul_left_cancel_nonzero (g * (Z * Z))
  18. 0018apply mul_left_cancel_nonzero
  19. 0019exact hg
  20. 0020trans a * b
  21. 0021rewrite ha
  22. 0022symm
  23. 0023apply mul_assoc
  24. 0024trans z * z
  25. 0025exact heq
  26. 0026rewrite hz
  27. 0027rewrite hz
  28. 0028trans (g * g) * (Z * Z)
  29. 0029apply four_square_product_square
  30. 0030apply mul_assoc
  31. 0031have hZA : forall frp_divisor_csf_reduced_swapped. (exists frp_left_factor_csf_reduced_swapped. Z = frp_divisor_csf_reduced_swapped * frp_left_factor_csf_reduced_swapped) -> (exists frp_right_factor_csf_reduced_swapped. A = frp_divisor_csf_reduced_swapped * frp_right_factor_csf_reduced_swapped) -> frp_divisor_csf_reduced_swapped = 1
  32. 0032specialize coprime_symm A
  33. 0033specialize coprime_symm Z
  34. 0034apply coprime_symm
  35. 0035exact hAZ
  36. 0036have hZsquareA : forall d. (exists x. Z * Z = d * x) -> (exists y. A = d * y) -> d = 1
  37. 0037specialize coprime_mul_left Z
  38. 0038specialize coprime_mul_left Z
  39. 0039specialize coprime_mul_left A
  40. 0040apply coprime_mul_left
  41. 0041exact hZA
  42. 0042exact hZA
  43. 0043have hbquot : exists k. b = (Z * Z) * k
  44. 0044specialize gauss_coprime_cancel (Z * Z)
  45. 0045specialize gauss_coprime_cancel A
  46. 0046specialize gauss_coprime_cancel b
  47. 0047apply gauss_coprime_cancel
  48. 0048exact hZsquareA
  49. 0049exists g
  50. 0050trans g * (Z * Z)
  51. 0051exact hreduced
  52. 0052apply mul_comm
  53. 0053cases hbquot
  54. 0054have hscale : A * x = g
  55. 0055specialize mul_right_cancel_nonzero (A * x)
  56. 0056specialize mul_right_cancel_nonzero g
  57. 0057specialize mul_right_cancel_nonzero (Z * Z)
  58. 0058apply mul_right_cancel_nonzero
  59. 0059intro hzero
  60. 0060specialize four_square_descent_nonzero_square Z
  61. 0061apply four_square_descent_nonzero_square
  62. 0062exact hZ
  63. 0063exact hzero
  64. 0064trans A * b
  65. 0065rewrite hbquot_witness
  66. 0066trans A * (x * (Z * Z))
  67. 0067apply mul_assoc
  68. 0068congr
  69. 0069refl
  70. 0070apply mul_comm
  71. 0071exact hreduced
  72. 0072have haquot : a = x * (A * A)
  73. 0073trans g * A
  74. 0074exact ha
  75. 0075rewrite <- hscale
  76. 0076trans (x * A) * A
  77. 0077congr
  78. 0078apply mul_comm
  79. 0079refl
  80. 0080apply mul_assoc
  81. 0081have hxone : x = 1
  82. 0082specialize hab x
  83. 0083apply hab
  84. 0084exists (A * A)
  85. 0085exact haquot
  86. 0086exists (Z * Z)
  87. 0087trans (Z * Z) * x
  88. 0088exact hbquot_witness
  89. 0089apply mul_comm
  90. 0090split
  91. 0091rewrite hxone at haquot
  92. 0092trans 1 * (A * A)
  93. 0093exact haquot
  94. 0094apply one_mul
  95. 0095rewrite hxone at hbquot_witness
  96. 0096trans (Z * Z) * 1
  97. 0097exact hbquot_witness
  98. 0098apply mul_one