MX000E

coprime_divisor_factor_pair_unique

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

The positive-divisor product map is injective on genuine divisor pairs of coprime inputs.

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

forall m n d a b c e. (forall sfd_common_divisor_cdp_unique_coprime. (exists pvs_factor_cdp_unique_coprimeleft. (m) = (sfd_common_divisor_cdp_unique_coprime) * pvs_factor_cdp_unique_coprimeleft) -> (exists pvs_factor_cdp_unique_coprimeright. (n) = (sfd_common_divisor_cdp_unique_coprime) * pvs_factor_cdp_unique_coprimeright) -> sfd_common_divisor_cdp_unique_coprime = 1) -> (((~((a)=0)) /\ (((~((b)=0)) /\ (((exists pvs_factor_cdp_unique_firstleft. (m) = (a) * pvs_factor_cdp_unique_firstleft) /\ (((exists pvs_factor_cdp_unique_firstright. (n) = (b) * pvs_factor_cdp_unique_firstright) /\ ((d)=(a)*(b)))))))))) -> (((~((c)=0)) /\ (((~((e)=0)) /\ (((exists pvs_factor_cdp_unique_secondleft. (m) = (c) * pvs_factor_cdp_unique_secondleft) /\ (((exists pvs_factor_cdp_unique_secondright. (n) = (e) * pvs_factor_cdp_unique_secondright) /\ ((d)=(c)*(e)))))))))) -> ((a=c) /\ (b=e))

Constructive proof overview

Generated structural guide

The positive-divisor product map is injective on genuine divisor pairs of coprime inputs.

The unchanged tactic script uses 2 declared prerequisites and contains 45 exact native proof lines.

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

Proof neighborhood

Direct dependencies

MX000D coprime_divisor_factor_pair_coordinates is_gcd_unique Stable theorem; checked-use authorized

Direct dependents

MX0011 coprime_divisor_factor_pair_exists_unique MX0053 dirichlet_coprime_grid_support_injective

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

45 script commands · 7 reading checkpoints · 2 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)
coprime divisor factor pair coordinates

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro m
  2. L2
    intro n
  3. L3
    intro d
  4. L4
    intro a
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro e
  8. L8
    intro hc
  9. L9
    intro hp
  10. L10
    intro hq
02Establish hpcoordsL11–19

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

  1. L11
    have hpcoords : IsGCD(a,m,d) ∧ IsGCD(b,n,d)Definitions: IsGCD
  2. L12
    specialize coprime_divisor_factor_pair_coordinates (m)
  3. L13
    specialize coprime_divisor_factor_pair_coordinates (n)
  4. L14
    specialize coprime_divisor_factor_pair_coordinates (d)
  5. L15
    specialize coprime_divisor_factor_pair_coordinates (a)
  6. L16
    specialize coprime_divisor_factor_pair_coordinates (b)
  7. L17
    apply coprime_divisor_factor_pair_coordinates
  8. L18
    exact hc
  9. L19
    exact hp
03Separate the logical casesL20–20

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

  1. L20
    cases hpcoords
04Establish hqcoordsL21–29

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

  1. L21
    have hqcoords : IsGCD(c,m,d) ∧ IsGCD(e,n,d)Definitions: IsGCD
  2. L22
    specialize coprime_divisor_factor_pair_coordinates (m)
  3. L23
    specialize coprime_divisor_factor_pair_coordinates (n)
  4. L24
    specialize coprime_divisor_factor_pair_coordinates (d)
  5. L25
    specialize coprime_divisor_factor_pair_coordinates (c)
  6. L26
    specialize coprime_divisor_factor_pair_coordinates (e)
  7. L27
    apply coprime_divisor_factor_pair_coordinates
  8. L28
    exact hc
  9. L29
    exact hq
05Separate the logical casesL30–31

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

  1. L30
    cases hqcoords
  2. L31
    split
06Use earlier factsL32–41

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

  1. L32
    specialize is_gcd_unique (a)
  2. L33
    specialize is_gcd_unique (c)
  3. L34
    specialize is_gcd_unique (m)
  4. L35
    specialize is_gcd_unique (d)
  5. L36
    apply is_gcd_unique
  6. L37
    exact hpcoords_left
  7. L38
    exact hqcoords_left
  8. L39
    specialize is_gcd_unique (b)
  9. L40
    specialize is_gcd_unique (e)
  10. L41
    specialize is_gcd_unique (n)
07Use earlier factsL42–45

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

  1. L42
    specialize is_gcd_unique (d)
  2. L43
    apply is_gcd_unique
  3. L44
    exact hpcoords_right
  4. L45
    exact hqcoords_right

Library-wide reading audit

Original exact command ledger · 45 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro d
  4. 0004intro a
  5. 0005intro b
  6. 0006intro c
  7. 0007intro e
  8. 0008intro hc
  9. 0009intro hp
  10. 0010intro hq
  11. 0011have hpcoords : (((((exists ec_gcd_left_cor_cdp_unique_pleft. m = a * ec_gcd_left_cor_cdp_unique_pleft) /\ (exists ec_gcd_right_cor_cdp_unique_pleft. d = a * ec_gcd_right_cor_cdp_unique_pleft)) /\ forall ec_gcd_common_cor_cdp_unique_pleft. (exists ec_gcd_common_left_cor_cdp_unique_pleft. m = ec_gcd_common_cor_cdp_unique_pleft * ec_gcd_common_left_cor_cdp_unique_pleft) -> (exists ec_gcd_common_right_cor_cdp_unique_pleft. d = ec_gcd_common_cor_cdp_unique_pleft * ec_gcd_common_right_cor_cdp_unique_pleft) -> exists ec_gcd_greatest_cor_cdp_unique_pleft. a = ec_gcd_common_cor_cdp_unique_pleft * ec_gcd_greatest_cor_cdp_unique_pleft)) /\ ((((exists ec_gcd_left_cor_cdp_unique_pright. n = b * ec_gcd_left_cor_cdp_unique_pright) /\ (exists ec_gcd_right_cor_cdp_unique_pright. d = b * ec_gcd_right_cor_cdp_unique_pright)) /\ forall ec_gcd_common_cor_cdp_unique_pright. (exists ec_gcd_common_left_cor_cdp_unique_pright. n = ec_gcd_common_cor_cdp_unique_pright * ec_gcd_common_left_cor_cdp_unique_pright) -> (exists ec_gcd_common_right_cor_cdp_unique_pright. d = ec_gcd_common_cor_cdp_unique_pright * ec_gcd_common_right_cor_cdp_unique_pright) -> exists ec_gcd_greatest_cor_cdp_unique_pright. b = ec_gcd_common_cor_cdp_unique_pright * ec_gcd_greatest_cor_cdp_unique_pright)))
  12. 0012specialize coprime_divisor_factor_pair_coordinates (m)
  13. 0013specialize coprime_divisor_factor_pair_coordinates (n)
  14. 0014specialize coprime_divisor_factor_pair_coordinates (d)
  15. 0015specialize coprime_divisor_factor_pair_coordinates (a)
  16. 0016specialize coprime_divisor_factor_pair_coordinates (b)
  17. 0017apply coprime_divisor_factor_pair_coordinates
  18. 0018exact hc
  19. 0019exact hp
  20. 0020cases hpcoords
  21. 0021have hqcoords : (((((exists ec_gcd_left_cor_cdp_unique_qleft. m = c * ec_gcd_left_cor_cdp_unique_qleft) /\ (exists ec_gcd_right_cor_cdp_unique_qleft. d = c * ec_gcd_right_cor_cdp_unique_qleft)) /\ forall ec_gcd_common_cor_cdp_unique_qleft. (exists ec_gcd_common_left_cor_cdp_unique_qleft. m = ec_gcd_common_cor_cdp_unique_qleft * ec_gcd_common_left_cor_cdp_unique_qleft) -> (exists ec_gcd_common_right_cor_cdp_unique_qleft. d = ec_gcd_common_cor_cdp_unique_qleft * ec_gcd_common_right_cor_cdp_unique_qleft) -> exists ec_gcd_greatest_cor_cdp_unique_qleft. c = ec_gcd_common_cor_cdp_unique_qleft * ec_gcd_greatest_cor_cdp_unique_qleft)) /\ ((((exists ec_gcd_left_cor_cdp_unique_qright. n = e * ec_gcd_left_cor_cdp_unique_qright) /\ (exists ec_gcd_right_cor_cdp_unique_qright. d = e * ec_gcd_right_cor_cdp_unique_qright)) /\ forall ec_gcd_common_cor_cdp_unique_qright. (exists ec_gcd_common_left_cor_cdp_unique_qright. n = ec_gcd_common_cor_cdp_unique_qright * ec_gcd_common_left_cor_cdp_unique_qright) -> (exists ec_gcd_common_right_cor_cdp_unique_qright. d = ec_gcd_common_cor_cdp_unique_qright * ec_gcd_common_right_cor_cdp_unique_qright) -> exists ec_gcd_greatest_cor_cdp_unique_qright. e = ec_gcd_common_cor_cdp_unique_qright * ec_gcd_greatest_cor_cdp_unique_qright)))
  22. 0022specialize coprime_divisor_factor_pair_coordinates (m)
  23. 0023specialize coprime_divisor_factor_pair_coordinates (n)
  24. 0024specialize coprime_divisor_factor_pair_coordinates (d)
  25. 0025specialize coprime_divisor_factor_pair_coordinates (c)
  26. 0026specialize coprime_divisor_factor_pair_coordinates (e)
  27. 0027apply coprime_divisor_factor_pair_coordinates
  28. 0028exact hc
  29. 0029exact hq
  30. 0030cases hqcoords
  31. 0031split
  32. 0032specialize is_gcd_unique (a)
  33. 0033specialize is_gcd_unique (c)
  34. 0034specialize is_gcd_unique (m)
  35. 0035specialize is_gcd_unique (d)
  36. 0036apply is_gcd_unique
  37. 0037exact hpcoords_left
  38. 0038exact hqcoords_left
  39. 0039specialize is_gcd_unique (b)
  40. 0040specialize is_gcd_unique (e)
  41. 0041specialize is_gcd_unique (n)
  42. 0042specialize is_gcd_unique (d)
  43. 0043apply is_gcd_unique
  44. 0044exact hpcoords_right
  45. 0045exact hqcoords_right