SK000F

squarefree_decomposition_functional

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

Gcd reduction, coprime square cancellation and squarefreeness prove literal uniqueness of both the squarefree kernel and its natural square-factor root.

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 n r s u v. ~(n = 0) -> (((~((r) = 0)) /\ (forall sfd_prime_unique_first. (~((sfd_prime_unique_first) = 1) /\ forall pvs_left_unique_firstdomain pvs_right_unique_firstdomain. (sfd_prime_unique_first) = pvs_left_unique_firstdomain * pvs_right_unique_firstdomain -> pvs_left_unique_firstdomain = 1 \/ pvs_right_unique_firstdomain = 1) -> (exists pvs_le_gap_unique_firstbound. pvs_le_gap_unique_firstbound + (sfd_prime_unique_first) = (r)) -> ~(exists pvs_factor_unique_firstsquare. (r) = (sfd_prime_unique_first * sfd_prime_unique_first) * pvs_factor_unique_firstsquare)))) -> (((~((u) = 0)) /\ (forall sfd_prime_unique_second. (~((sfd_prime_unique_second) = 1) /\ forall pvs_left_unique_seconddomain pvs_right_unique_seconddomain. (sfd_prime_unique_second) = pvs_left_unique_seconddomain * pvs_right_unique_seconddomain -> pvs_left_unique_seconddomain = 1 \/ pvs_right_unique_seconddomain = 1) -> (exists pvs_le_gap_unique_secondbound. pvs_le_gap_unique_secondbound + (sfd_prime_unique_second) = (u)) -> ~(exists pvs_factor_unique_secondsquare. (u) = (sfd_prime_unique_second * sfd_prime_unique_second) * pvs_factor_unique_secondsquare)))) -> n = r * (s * s) -> n = u * (v * v) -> u = r /\ v = s

Constructive proof overview

Generated structural guide

Gcd reduction, coprime square cancellation and squarefreeness prove literal uniqueness of both the squarefree kernel and its natural square-factor root.

The unchanged tactic script uses 10 declared prerequisites and contains 103 exact native proof lines.

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

Proof neighborhood

Direct dependencies

SK0008 nonzero_square_factor_root canonical_gcd_exists Alpha theorem; checked-use authorized is_gcd_dvd_left Stable theorem; checked-use authorized is_gcd_dvd_right Stable theorem; checked-use authorized factor_nonzero_left Stable theorem; checked-use authorized is_gcd_quotients_coprime_nonzero Stable theorem; checked-use authorized four_square_descent_square_factor_cancel Alpha theorem; checked-use authorized SK0007 squarefree_square_factor_reassociate SK000E squarefree_coprime_square_balance mul_one Stable theorem; checked-use authorized

Direct dependents

SK0010 squarefree_decomposition_exists_unique

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

103 script commands · 25 reading checkpoints · 8 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 (3)
nonzero square factor rootsquarefree square factor reassociatesquarefree coprime square balance
01Fix variables and assumptionsL1–10

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

  1. L1
    intro n
  2. L2
    intro r
  3. L3
    intro s
  4. L4
    intro u
  5. L5
    intro v
  6. L6
    intro hn
  7. L7
    intro hr
  8. L8
    intro hu
  9. L9
    intro heqr
  10. L10
    intro hequ
02Establish hsnonzeroL11–19

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

  1. L11
    have hsnonzero : ~(s = 0)
  2. L12
    intro hz
  3. L13
    specialize nonzero_square_factor_root (n)
  4. L14
    specialize nonzero_square_factor_root (r)
  5. L15
    specialize nonzero_square_factor_root (s)
  6. L16
    apply nonzero_square_factor_root
  7. L17
    exact hn
  8. L18
    exact heqr
  9. L19
    exact hz
03Establish hgL20–23

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

  1. L20
    have hg : exists g. ((((exists hag_left_factor_sfd_unique_gcd. s = g * hag_left_factor_sfd_unique_gcd) /\ (exists hag_right_factor_sfd_unique_gcd. v = g * hag_right_factor_sfd_unique_gcd)) /\ forall hag_divisor_sfd_unique_gcd. (exists hag_common_left_sfd_unique_gcd. s = hag_divisor_sfd_unique_gcd * hag_common_left_sfd_unique_gcd) -> (exists hag_common_right_sfd_unique_gcd. v = hag_divisor_sfd_unique_gcd * hag_common_right_sfd_unique_gcd) -> exists hag_greatest_factor_sfd_unique_gcd. g = hag_divisor_sfd_unique_gcd * hag_greatest_factor_sfd_unique_gcd))
  2. L21
    specialize canonical_gcd_exists (s)
  3. L22
    specialize canonical_gcd_exists (v)
  4. L23
    apply canonical_gcd_exists
04Separate the logical casesL24–24

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

  1. L24
    cases hg
05Establish hsL25–30

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

  1. L25
    have hs : exists A. s = x * A
  2. L26
    specialize is_gcd_dvd_left (x)
  3. L27
    specialize is_gcd_dvd_left (s)
  4. L28
    specialize is_gcd_dvd_left (v)
  5. L29
    apply is_gcd_dvd_left
  6. L30
    exact hg_witness
06Separate the logical casesL31–31

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

  1. L31
    cases hs
07Establish hvL32–37

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

  1. L32
    have hv : exists B. v = x * B
  2. L33
    specialize is_gcd_dvd_right (x)
  3. L34
    specialize is_gcd_dvd_right (s)
  4. L35
    specialize is_gcd_dvd_right (v)
  5. L36
    apply is_gcd_dvd_right
  6. L37
    exact hg_witness
08Separate the logical casesL38–38

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

  1. L38
    cases hv
09Establish hgnonzeroL39–47

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

  1. L39
    have hgnonzero : ~(x = 0)
  2. L40
    intro hgzero
  3. L41
    specialize factor_nonzero_left (s)
  4. L42
    specialize factor_nonzero_left (x)
  5. L43
    specialize factor_nonzero_left (x1)
  6. L44
    apply factor_nonzero_left
  7. L45
    exact hsnonzero
  8. L46
    exact hs_witness
  9. L47
    exact hgzero
10Establish hcopL48–57

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

  1. L48
    have hcop : forall sfd_common_divisor_unique_coprime. (exists pvs_factor_unique_coprimeleft. (x1) = (sfd_common_divisor_unique_coprime) * pvs_factor_unique_coprimeleft) -> (exists pvs_factor_unique_coprimeright. (x2) = (sfd_common_divisor_unique_coprime) * pvs_factor_unique_coprimeright) -> sfd_common_divisor_unique_coprime = 1
  2. L49
    specialize is_gcd_quotients_coprime_nonzero (x)
  3. L50
    specialize is_gcd_quotients_coprime_nonzero (s)
  4. L51
    specialize is_gcd_quotients_coprime_nonzero (v)
  5. L52
    specialize is_gcd_quotients_coprime_nonzero (x1)
  6. L53
    specialize is_gcd_quotients_coprime_nonzero (x2)
  7. L54
    apply is_gcd_quotients_coprime_nonzero
  8. L55
    exact hg_witness
  9. L56
    exact hgnonzero
  10. L57
    exact hs_witness
11Use earlier factsL58–58

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

  1. L58
    exact hv_witness
12Establish hbalanceL59–68

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square descent square factor cancel.

  1. L59
    have hbalance : r * (x1 * x1) = u * (x2 * x2)
  2. L60
    specialize four_square_descent_square_factor_cancel (x)
  3. L61
    specialize four_square_descent_square_factor_cancel (r * (x1 * x1))
  4. L62
    specialize four_square_descent_square_factor_cancel (u * (x2 * x2))
  5. L63
    apply four_square_descent_square_factor_cancel
  6. L64
    exact hgnonzero
  7. L65
    trans n
  8. L66
    trans r * ((x * x1) * (x * x1))
  9. L67
    apply squarefree_square_factor_reassociate
  10. L68
    trans r * (s * s)
13Calculate and transport equalitiesL69–72

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

  1. L69
    rewrite hs_witness
  2. L70
    rewrite hs_witness
  3. L71
    refl
  4. L72
    symm
14Use earlier factsL73–73

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

  1. L73
    exact heqr
15Calculate and transport equalitiesL74–74

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

  1. L74
    trans u * (v * v)
16Use earlier factsL75–75

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

  1. L75
    exact hequ
17Calculate and transport equalitiesL76–80

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

  1. L76
    trans u * ((x * x2) * (x * x2))
  2. L77
    rewrite hv_witness
  3. L78
    rewrite hv_witness
  4. L79
    refl
  5. L80
    symm
18Use earlier factsL81–81

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

  1. L81
    apply squarefree_square_factor_reassociate
19Establish hunitL82–91

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

  1. L82
    have hunit : u = r /\ (x1 = 1 /\ x2 = 1)
  2. L83
    specialize squarefree_coprime_square_balance (r)
  3. L84
    specialize squarefree_coprime_square_balance (u)
  4. L85
    specialize squarefree_coprime_square_balance (x1)
  5. L86
    specialize squarefree_coprime_square_balance (x2)
  6. L87
    apply squarefree_coprime_square_balance
  7. L88
    exact hr
  8. L89
    exact hu
  9. L90
    exact hcop
  10. L91
    exact hbalance
20Separate the logical casesL92–94

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

  1. L92
    cases hunit
  2. L93
    cases hunit_right
  3. L94
    split
21Use earlier factsL95–95

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

  1. L95
    exact hunit_left
22Calculate and transport equalitiesL96–98

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

  1. L96
    trans x
  2. L97
    rewrite hv_witness
  3. L98
    rewrite hunit_right_right
23Use earlier factsL99–99

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

  1. L99
    apply mul_one
24Calculate and transport equalitiesL100–102

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

  1. L100
    symm
  2. L101
    rewrite hs_witness
  3. L102
    rewrite hunit_right_left
25Use earlier factsL103–103

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

  1. L103
    apply mul_one

Library-wide reading audit

Original exact command ledger · 103 lines
  1. 0001intro n
  2. 0002intro r
  3. 0003intro s
  4. 0004intro u
  5. 0005intro v
  6. 0006intro hn
  7. 0007intro hr
  8. 0008intro hu
  9. 0009intro heqr
  10. 0010intro hequ
  11. 0011have hsnonzero : ~(s = 0)
  12. 0012intro hz
  13. 0013specialize nonzero_square_factor_root (n)
  14. 0014specialize nonzero_square_factor_root (r)
  15. 0015specialize nonzero_square_factor_root (s)
  16. 0016apply nonzero_square_factor_root
  17. 0017exact hn
  18. 0018exact heqr
  19. 0019exact hz
  20. 0020have hg : exists g. ((((exists hag_left_factor_sfd_unique_gcd. s = g * hag_left_factor_sfd_unique_gcd) /\ (exists hag_right_factor_sfd_unique_gcd. v = g * hag_right_factor_sfd_unique_gcd)) /\ forall hag_divisor_sfd_unique_gcd. (exists hag_common_left_sfd_unique_gcd. s = hag_divisor_sfd_unique_gcd * hag_common_left_sfd_unique_gcd) -> (exists hag_common_right_sfd_unique_gcd. v = hag_divisor_sfd_unique_gcd * hag_common_right_sfd_unique_gcd) -> exists hag_greatest_factor_sfd_unique_gcd. g = hag_divisor_sfd_unique_gcd * hag_greatest_factor_sfd_unique_gcd))
  21. 0021specialize canonical_gcd_exists (s)
  22. 0022specialize canonical_gcd_exists (v)
  23. 0023apply canonical_gcd_exists
  24. 0024cases hg
  25. 0025have hs : exists A. s = x * A
  26. 0026specialize is_gcd_dvd_left (x)
  27. 0027specialize is_gcd_dvd_left (s)
  28. 0028specialize is_gcd_dvd_left (v)
  29. 0029apply is_gcd_dvd_left
  30. 0030exact hg_witness
  31. 0031cases hs
  32. 0032have hv : exists B. v = x * B
  33. 0033specialize is_gcd_dvd_right (x)
  34. 0034specialize is_gcd_dvd_right (s)
  35. 0035specialize is_gcd_dvd_right (v)
  36. 0036apply is_gcd_dvd_right
  37. 0037exact hg_witness
  38. 0038cases hv
  39. 0039have hgnonzero : ~(x = 0)
  40. 0040intro hgzero
  41. 0041specialize factor_nonzero_left (s)
  42. 0042specialize factor_nonzero_left (x)
  43. 0043specialize factor_nonzero_left (x1)
  44. 0044apply factor_nonzero_left
  45. 0045exact hsnonzero
  46. 0046exact hs_witness
  47. 0047exact hgzero
  48. 0048have hcop : forall sfd_common_divisor_unique_coprime. (exists pvs_factor_unique_coprimeleft. (x1) = (sfd_common_divisor_unique_coprime) * pvs_factor_unique_coprimeleft) -> (exists pvs_factor_unique_coprimeright. (x2) = (sfd_common_divisor_unique_coprime) * pvs_factor_unique_coprimeright) -> sfd_common_divisor_unique_coprime = 1
  49. 0049specialize is_gcd_quotients_coprime_nonzero (x)
  50. 0050specialize is_gcd_quotients_coprime_nonzero (s)
  51. 0051specialize is_gcd_quotients_coprime_nonzero (v)
  52. 0052specialize is_gcd_quotients_coprime_nonzero (x1)
  53. 0053specialize is_gcd_quotients_coprime_nonzero (x2)
  54. 0054apply is_gcd_quotients_coprime_nonzero
  55. 0055exact hg_witness
  56. 0056exact hgnonzero
  57. 0057exact hs_witness
  58. 0058exact hv_witness
  59. 0059have hbalance : r * (x1 * x1) = u * (x2 * x2)
  60. 0060specialize four_square_descent_square_factor_cancel (x)
  61. 0061specialize four_square_descent_square_factor_cancel (r * (x1 * x1))
  62. 0062specialize four_square_descent_square_factor_cancel (u * (x2 * x2))
  63. 0063apply four_square_descent_square_factor_cancel
  64. 0064exact hgnonzero
  65. 0065trans n
  66. 0066trans r * ((x * x1) * (x * x1))
  67. 0067apply squarefree_square_factor_reassociate
  68. 0068trans r * (s * s)
  69. 0069rewrite hs_witness
  70. 0070rewrite hs_witness
  71. 0071refl
  72. 0072symm
  73. 0073exact heqr
  74. 0074trans u * (v * v)
  75. 0075exact hequ
  76. 0076trans u * ((x * x2) * (x * x2))
  77. 0077rewrite hv_witness
  78. 0078rewrite hv_witness
  79. 0079refl
  80. 0080symm
  81. 0081apply squarefree_square_factor_reassociate
  82. 0082have hunit : u = r /\ (x1 = 1 /\ x2 = 1)
  83. 0083specialize squarefree_coprime_square_balance (r)
  84. 0084specialize squarefree_coprime_square_balance (u)
  85. 0085specialize squarefree_coprime_square_balance (x1)
  86. 0086specialize squarefree_coprime_square_balance (x2)
  87. 0087apply squarefree_coprime_square_balance
  88. 0088exact hr
  89. 0089exact hu
  90. 0090exact hcop
  91. 0091exact hbalance
  92. 0092cases hunit
  93. 0093cases hunit_right
  94. 0094split
  95. 0095exact hunit_left
  96. 0096trans x
  97. 0097rewrite hv_witness
  98. 0098rewrite hunit_right_right
  99. 0099apply mul_one
  100. 0100symm
  101. 0101rewrite hs_witness
  102. 0102rewrite hunit_right_left
  103. 0103apply mul_one