GC000E

crt_is_gcd_scale

Every common natural scale, including zero, transports the full relational greatest-common-divisor specification constructively.

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

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.

Historical partial components only: this chapter proves canonical solutions under successive-merge compatibility and in the pairwise-compatible dominating-last case. G011 is now closed in the separate Alpha-v27 generalized-crt branch for arbitrary pairwise-compatible finite lists, including noncoprime moduli. Full G011 proof · Alpha v27

Exact theorem in conservative defined notation

∀ k. ∀ a. ∀ b. ∀ g. ∀ A. ∀ B. ∀ G. A = k · a → B = k · b → G = k · g → IsGCD(g,a,b) → IsGCD(G,A,B)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

IsGCD(g,a,b) · 2

Actual proof prerequisites

is_gcd_dvd_left · checked external prerequisiteis_gcd_dvd_right · checked external prerequisitemul_assoc · checked external prerequisitegcd_balanced_bezout_exists · checked external prerequisiteis_gcd_unique · checked external prerequisitecrt_balanced_bezout_scalecommon_divisor_divides_balanced_result · checked external prerequisite
Original expanded first-order statement 
forall k a b g A B G. A = k * a -> B = k * b -> G = k * g -> ((((exists hag_left_factor_gcomp_gcd_scale_source. a = g * hag_left_factor_gcomp_gcd_scale_source) /\ (exists hag_right_factor_gcomp_gcd_scale_source. b = g * hag_right_factor_gcomp_gcd_scale_source)) /\ forall hag_divisor_gcomp_gcd_scale_source. (exists hag_common_left_gcomp_gcd_scale_source. a = hag_divisor_gcomp_gcd_scale_source * hag_common_left_gcomp_gcd_scale_source) -> (exists hag_common_right_gcomp_gcd_scale_source. b = hag_divisor_gcomp_gcd_scale_source * hag_common_right_gcomp_gcd_scale_source) -> exists hag_greatest_factor_gcomp_gcd_scale_source. g = hag_divisor_gcomp_gcd_scale_source * hag_greatest_factor_gcomp_gcd_scale_source)) -> ((((exists hag_left_factor_gcomp_gcd_scale_result. A = G * hag_left_factor_gcomp_gcd_scale_result) /\ (exists hag_right_factor_gcomp_gcd_scale_result. B = G * hag_right_factor_gcomp_gcd_scale_result)) /\ forall hag_divisor_gcomp_gcd_scale_result. (exists hag_common_left_gcomp_gcd_scale_result. A = hag_divisor_gcomp_gcd_scale_result * hag_common_left_gcomp_gcd_scale_result) -> (exists hag_common_right_gcomp_gcd_scale_result. B = hag_divisor_gcomp_gcd_scale_result * hag_common_right_gcomp_gcd_scale_result) -> exists hag_greatest_factor_gcomp_gcd_scale_result. G = hag_divisor_gcomp_gcd_scale_result * hag_greatest_factor_gcomp_gcd_scale_result))

Complete unchanged native tactic proof

All 87 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

87 script commands · 23 reading checkpoints · 4 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 (1)
crt balanced bezout scale
01Fix variables and assumptionsL1–10

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

  1. L1
    intro k
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro g
  5. L5
    intro A
  6. L6
    intro B
  7. L7
    intro G
  8. L8
    intro hA
  9. L9
    intro hB
  10. L10
    intro hG
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hg
03Establish hleftL12–17

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

  1. L12
    have hleft : exists q. a = g * q
  2. L13
    specialize is_gcd_dvd_left g
  3. L14
    specialize is_gcd_dvd_left a
  4. L15
    specialize is_gcd_dvd_left b
  5. L16
    apply is_gcd_dvd_left
  6. L17
    exact hg
04Separate the logical casesL18–18

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

  1. L18
    cases hleft
05Establish hrightL19–24

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

  1. L19
    have hright : exists q. b = g * q
  2. L20
    specialize is_gcd_dvd_right g
  3. L21
    specialize is_gcd_dvd_right a
  4. L22
    specialize is_gcd_dvd_right b
  5. L23
    apply is_gcd_dvd_right
  6. L24
    exact hg
06Separate the logical casesL25–25

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

  1. L25
    cases hright
07Use earlier factsL26–27

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

  1. L26
    specialize gcd_balanced_bezout_exists a
  2. L27
    specialize gcd_balanced_bezout_exists b
08Separate the logical casesL28–29

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

  1. L28
    cases gcd_balanced_bezout_exists
  2. L29
    cases gcd_balanced_bezout_exists_witness
09Establish heqL30–37

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

  1. L30
    have heq : x2 = g
  2. L31
    specialize is_gcd_unique x2
  3. L32
    specialize is_gcd_unique g
  4. L33
    specialize is_gcd_unique a
  5. L34
    specialize is_gcd_unique b
  6. L35
    apply is_gcd_unique
  7. L36
    exact gcd_balanced_bezout_exists_witness_left
  8. L37
    exact hg
10Separate the logical casesL38–41

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

  1. L38
    cases gcd_balanced_bezout_exists_witness_right
  2. L39
    cases gcd_balanced_bezout_exists_witness_right_witness
  3. L40
    cases gcd_balanced_bezout_exists_witness_right_witness_witness
  4. L41
    cases gcd_balanced_bezout_exists_witness_right_witness_witness_witness
11Calculate and transport equalitiesL42–42

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

  1. L42
    rewrite heq at gcd_balanced_bezout_exists_witness_right_witness_witness_witness_witness
12Establish hscaledL43–52

Establish this local claim before using it. It is not an additional assumption.

  1. L43
    have hscaled : A * x3 + B * x4 = G + (A * x5 + B * x6)
  2. L44
    rewrite hA
  3. L45
    rewrite hA
  4. L46
    rewrite hB
  5. L47
    rewrite hB
  6. L48
    rewrite hG
  7. L49
    specialize crt_balanced_bezout_scale k
  8. L50
    specialize crt_balanced_bezout_scale a
  9. L51
    specialize crt_balanced_bezout_scale b
  10. L52
    specialize crt_balanced_bezout_scale g
13Use earlier factsL53–58

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

  1. L53
    specialize crt_balanced_bezout_scale x3
  2. L54
    specialize crt_balanced_bezout_scale x4
  3. L55
    specialize crt_balanced_bezout_scale x5
  4. L56
    specialize crt_balanced_bezout_scale x6
  5. L57
    apply crt_balanced_bezout_scale
  6. L58
    exact gcd_balanced_bezout_exists_witness_right_witness_witness_witness_witness
14Separate the logical casesL59–60

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

  1. L59
    split
  2. L60
    split
15Construct an explicit witnessL61–61

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

  1. L61
    exists x
16Calculate and transport equalitiesL62–65

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

  1. L62
    rewrite hA
  2. L63
    rewrite hG
  3. L64
    rewrite hleft_witness
  4. L65
    symm
17Use earlier factsL66–66

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

  1. L66
    apply mul_assoc
18Construct an explicit witnessL67–67

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

  1. L67
    exists x1
19Calculate and transport equalitiesL68–71

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

  1. L68
    rewrite hB
  2. L69
    rewrite hG
  3. L70
    rewrite hright_witness
  4. L71
    symm
20Use earlier factsL72–72

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

  1. L72
    apply mul_assoc
21Fix variables and assumptionsL73–75

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

  1. L73
    intro d
  2. L74
    intro hdA
  3. L75
    intro hdB
22Use earlier factsL76–85

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

  1. L76
    specialize common_divisor_divides_balanced_result d
  2. L77
    specialize common_divisor_divides_balanced_result A
  3. L78
    specialize common_divisor_divides_balanced_result B
  4. L79
    specialize common_divisor_divides_balanced_result G
  5. L80
    specialize common_divisor_divides_balanced_result x3
  6. L81
    specialize common_divisor_divides_balanced_result x4
  7. L82
    specialize common_divisor_divides_balanced_result x5
  8. L83
    specialize common_divisor_divides_balanced_result x6
  9. L84
    apply common_divisor_divides_balanced_result
  10. L85
    exact hdA
23Use earlier factsL86–87

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

  1. L86
    exact hdB
  2. L87
    exact hscaled

Library-wide reading audit

Original defined command ledger · 87 lines
  1. 0001intro k
  2. 0002intro a
  3. 0003intro b
  4. 0004intro g
  5. 0005intro A
  6. 0006intro B
  7. 0007intro G
  8. 0008intro hA
  9. 0009intro hB
  10. 0010intro hG
  11. 0011intro hg
  12. 0012have hleft : exists q. a = g * q
  13. 0013specialize is_gcd_dvd_left g
  14. 0014specialize is_gcd_dvd_left a
  15. 0015specialize is_gcd_dvd_left b
  16. 0016apply is_gcd_dvd_left
  17. 0017exact hg
  18. 0018cases hleft
  19. 0019have hright : exists q. b = g * q
  20. 0020specialize is_gcd_dvd_right g
  21. 0021specialize is_gcd_dvd_right a
  22. 0022specialize is_gcd_dvd_right b
  23. 0023apply is_gcd_dvd_right
  24. 0024exact hg
  25. 0025cases hright
  26. 0026specialize gcd_balanced_bezout_exists a
  27. 0027specialize gcd_balanced_bezout_exists b
  28. 0028cases gcd_balanced_bezout_exists
  29. 0029cases gcd_balanced_bezout_exists_witness
  30. 0030have heq : x2 = g
  31. 0031specialize is_gcd_unique x2
  32. 0032specialize is_gcd_unique g
  33. 0033specialize is_gcd_unique a
  34. 0034specialize is_gcd_unique b
  35. 0035apply is_gcd_unique
  36. 0036exact gcd_balanced_bezout_exists_witness_left
  37. 0037exact hg
  38. 0038cases gcd_balanced_bezout_exists_witness_right
  39. 0039cases gcd_balanced_bezout_exists_witness_right_witness
  40. 0040cases gcd_balanced_bezout_exists_witness_right_witness_witness
  41. 0041cases gcd_balanced_bezout_exists_witness_right_witness_witness_witness
  42. 0042rewrite heq at gcd_balanced_bezout_exists_witness_right_witness_witness_witness_witness
  43. 0043have hscaled : A * x3 + B * x4 = G + (A * x5 + B * x6)
  44. 0044rewrite hA
  45. 0045rewrite hA
  46. 0046rewrite hB
  47. 0047rewrite hB
  48. 0048rewrite hG
  49. 0049specialize crt_balanced_bezout_scale k
  50. 0050specialize crt_balanced_bezout_scale a
  51. 0051specialize crt_balanced_bezout_scale b
  52. 0052specialize crt_balanced_bezout_scale g
  53. 0053specialize crt_balanced_bezout_scale x3
  54. 0054specialize crt_balanced_bezout_scale x4
  55. 0055specialize crt_balanced_bezout_scale x5
  56. 0056specialize crt_balanced_bezout_scale x6
  57. 0057apply crt_balanced_bezout_scale
  58. 0058exact gcd_balanced_bezout_exists_witness_right_witness_witness_witness_witness
  59. 0059split
  60. 0060split
  61. 0061exists x
  62. 0062rewrite hA
  63. 0063rewrite hG
  64. 0064rewrite hleft_witness
  65. 0065symm
  66. 0066apply mul_assoc
  67. 0067exists x1
  68. 0068rewrite hB
  69. 0069rewrite hG
  70. 0070rewrite hright_witness
  71. 0071symm
  72. 0072apply mul_assoc
  73. 0073intro d
  74. 0074intro hdA
  75. 0075intro hdB
  76. 0076specialize common_divisor_divides_balanced_result d
  77. 0077specialize common_divisor_divides_balanced_result A
  78. 0078specialize common_divisor_divides_balanced_result B
  79. 0079specialize common_divisor_divides_balanced_result G
  80. 0080specialize common_divisor_divides_balanced_result x3
  81. 0081specialize common_divisor_divides_balanced_result x4
  82. 0082specialize common_divisor_divides_balanced_result x5
  83. 0083specialize common_divisor_divides_balanced_result x6
  84. 0084apply common_divisor_divides_balanced_result
  85. 0085exact hdA
  86. 0086exact hdB
  87. 0087exact hscaled