CG0003

linear_congruence_reduced_representative_exists

Construct a genuine solution strictly below m/g, not merely below m, from the actual gcd divisibility witness.

Alpha v34 checked-use · first admitted v34 · 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.

Each statement retains its explicit modulus, coprimality and divisibility assumptions. These twelve arithmetic laws do not assert all order, primitive-root, Carmichael, exponential or simultaneous-polynomial congruence goals are finished.

Exact theorem in conservative defined notation

∀ a. ∀ m. ∀ g. ∀ A. ∀ M. ∀ b. ¬m = 0 → IsGCD(g,a,m) → a = g · A → m = g · M → Dvd(g,b) → ∃ x. Lt(x,M) ∧ ModEq(m,a · x,b)

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

Definition DAG

Lt(a,b) · 1Dvd(d,n) · 1IsGCD(g,a,b) · 1DivRem(n,d,q,r) · 1ModEq(m,a,b) · 7

Actual proof prerequisites

mul_zero_left · checked external prerequisitelinear_congruence_gcd_divisibility_constructs_solution · checked external prerequisitedivision_remainder_exists · checked external prerequisitemod_eq_symm · checked external prerequisiteremainder_decomposition_to_mod_eq · checked external prerequisitemul_comm · checked external prerequisitelinear_congruence_solution_class_iff_reduced_modulus
Original expanded first-order statement 
forall a m g A M b. (~(m=0)) -> ((((exists hag_left_factor_lcc_representative. a = g * hag_left_factor_lcc_representative) /\ (exists hag_right_factor_lcc_representative. m = g * hag_right_factor_lcc_representative)) /\ forall hag_divisor_lcc_representative. (exists hag_common_left_lcc_representative. a = hag_divisor_lcc_representative * hag_common_left_lcc_representative) -> (exists hag_common_right_lcc_representative. m = hag_divisor_lcc_representative * hag_common_right_lcc_representative) -> exists hag_greatest_factor_lcc_representative. g = hag_divisor_lcc_representative * hag_greatest_factor_lcc_representative)) -> (a=g*A) -> (m=g*M) -> (exists lcc_bfactor. b=g*lcc_bfactor) -> (exists r. ((exists lcc_gap_representative_bound. lcc_gap_representative_bound+S (r)=(M)) /\ ((exists hgcrt_mod_left_lcc_representative_solution hgcrt_mod_right_lcc_representative_solution. (a * r) + m * hgcrt_mod_left_lcc_representative_solution = b + m * hgcrt_mod_right_lcc_representative_solution))))

Complete tactic proof in conservative notation

All 78 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

78 script commands · 21 reading checkpoints · 6 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)
linear congruence solution class iff reduced modulus
01Fix variables and assumptionsL1–10

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

  1. L1
    intro a
  2. L2
    intro m
  3. L3
    intro g
  4. L4
    intro A
  5. L5
    intro M
  6. L6
    intro b
  7. L7
    intro hm0
  8. L8
    intro hg
  9. L9
    intro ha
  10. L10
    intro hm
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hb
03Establish hg0L12–18

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

  1. L12
    have hg0 : ~(g=0)
  2. L13
    intro hz
  3. L14
    apply hm0
  4. L15
    trans g*M
  5. L16
    exact hm
  6. L17
    rewrite hz
  7. L18
    apply mul_zero_left
04Establish hM0L19–25

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

  1. L19
    have hM0 : ~(M=0)
  2. L20
    intro hz
  3. L21
    apply hm0
  4. L22
    trans g*M
  5. L23
    exact hm
  6. L24
    rewrite hz
  7. L25
    simp
05Establish hsL26–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply linear congruence gcd divisibility constructs solution.

  1. L26
    have hs : ∃ x. ModEq(m,a · x,b)Definitions: ModEq(m,a · x,b)Original native command in the exact edition
  2. L27
    specialize linear_congruence_gcd_divisibility_constructs_solution (a)
  3. L28
    specialize linear_congruence_gcd_divisibility_constructs_solution (m)
  4. L29
    specialize linear_congruence_gcd_divisibility_constructs_solution (b)
  5. L30
    specialize linear_congruence_gcd_divisibility_constructs_solution (g)
  6. L31
    apply linear_congruence_gcd_divisibility_constructs_solution
  7. L32
    exact hg
  8. L33
    exact hb
06Separate the logical casesL34–34

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

  1. L34
    cases hs
07Establish hdL35–39

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

  1. L35
    have hd : ∃ q. ∃ r. DivRem(x,M,q,r)Definitions: DivRem(x,M,q,r)Original native command in the exact edition
  2. L36
    specialize division_remainder_exists (M)
  3. L37
    specialize division_remainder_exists (x)
  4. L38
    apply division_remainder_exists
  5. L39
    exact hM0
08Separate the logical casesL40–42

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

  1. L40
    cases hd
  2. L41
    cases hd_witness
  3. L42
    cases hd_witness_witness
09Construct an explicit witnessL43–43

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

  1. L43
    exists x2
10Separate the logical casesL44–44

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

  1. L44
    split
11Use earlier factsL45–45

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

  1. L45
    exact hd_witness_witness_right
12Establish heL46–55

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

  1. L46
  2. L47
    specialize mod_eq_symm (M)
  3. L48
    specialize mod_eq_symm (x)
  4. L49
    specialize mod_eq_symm (x2)
  5. L50
    apply mod_eq_symm
  6. L51
    specialize remainder_decomposition_to_mod_eq (M)
  7. L52
    specialize remainder_decomposition_to_mod_eq (x)
  8. L53
    specialize remainder_decomposition_to_mod_eq (x1)
  9. L54
    specialize remainder_decomposition_to_mod_eq (x2)
  10. L55
    apply remainder_decomposition_to_mod_eq
13Calculate and transport equalitiesL56–56

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

  1. L56
    trans M*x1+x2
14Use earlier factsL57–57

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

  1. L57
    exact hd_witness_witness_left
15Calculate and transport equalitiesL58–58

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

  1. L58
    congr
16Use earlier factsL59–59

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

  1. L59
    apply mul_comm
17Calculate and transport equalitiesL60–60

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

  1. L60
    refl
18Establish hcL61–70

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply linear congruence solution class iff reduced modulus.

  1. L61
    have hc : (ModEq(m,a · x2,b) → ModEq(M,x2,x)) ∧ (ModEq(M,x2,x) → ModEq(m,a · x2,b))Definitions: ModEq(m,a · x2,b)ModEq(M,x2,x)Original native command in the exact edition
  2. L62
    specialize linear_congruence_solution_class_iff_reduced_modulus (a)
  3. L63
    specialize linear_congruence_solution_class_iff_reduced_modulus (m)
  4. L64
    specialize linear_congruence_solution_class_iff_reduced_modulus (g)
  5. L65
    specialize linear_congruence_solution_class_iff_reduced_modulus (A)
  6. L66
    specialize linear_congruence_solution_class_iff_reduced_modulus (M)
  7. L67
    specialize linear_congruence_solution_class_iff_reduced_modulus (b)
  8. L68
    specialize linear_congruence_solution_class_iff_reduced_modulus (x)
  9. L69
    specialize linear_congruence_solution_class_iff_reduced_modulus (x2)
  10. L70
    apply linear_congruence_solution_class_iff_reduced_modulus
19Use earlier factsL71–75

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

  1. L71
    exact hm0
  2. L72
    exact hg
  3. L73
    exact ha
  4. L74
    exact hm
  5. L75
    exact hs_witness
20Separate the logical casesL76–76

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

  1. L76
    cases hc
21Use earlier factsL77–78

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

  1. L77
    apply hc_right
  2. L78
    exact he

Library-wide reading audit

Original defined command ledger · 78 lines
  1. 0001intro a
  2. 0002intro m
  3. 0003intro g
  4. 0004intro A
  5. 0005intro M
  6. 0006intro b
  7. 0007intro hm0
  8. 0008intro hg
  9. 0009intro ha
  10. 0010intro hm
  11. 0011intro hb
  12. 0012have hg0 : ~(g=0)
  13. 0013intro hz
  14. 0014apply hm0
  15. 0015trans g*M
  16. 0016exact hm
  17. 0017rewrite hz
  18. 0018apply mul_zero_left
  19. 0019have hM0 : ~(M=0)
  20. 0020intro hz
  21. 0021apply hm0
  22. 0022trans g*M
  23. 0023exact hm
  24. 0024rewrite hz
  25. 0025simp
  26. 0026have hs : ∃ x. ModEq(m,a · x,b)
  27. 0027specialize linear_congruence_gcd_divisibility_constructs_solution (a)
  28. 0028specialize linear_congruence_gcd_divisibility_constructs_solution (m)
  29. 0029specialize linear_congruence_gcd_divisibility_constructs_solution (b)
  30. 0030specialize linear_congruence_gcd_divisibility_constructs_solution (g)
  31. 0031apply linear_congruence_gcd_divisibility_constructs_solution
  32. 0032exact hg
  33. 0033exact hb
  34. 0034cases hs
  35. 0035have hd : ∃ q. ∃ r. DivRem(x,M,q,r)
  36. 0036specialize division_remainder_exists (M)
  37. 0037specialize division_remainder_exists (x)
  38. 0038apply division_remainder_exists
  39. 0039exact hM0
  40. 0040cases hd
  41. 0041cases hd_witness
  42. 0042cases hd_witness_witness
  43. 0043exists x2
  44. 0044split
  45. 0045exact hd_witness_witness_right
  46. 0046have he : ModEq(M,x2,x)
  47. 0047specialize mod_eq_symm (M)
  48. 0048specialize mod_eq_symm (x)
  49. 0049specialize mod_eq_symm (x2)
  50. 0050apply mod_eq_symm
  51. 0051specialize remainder_decomposition_to_mod_eq (M)
  52. 0052specialize remainder_decomposition_to_mod_eq (x)
  53. 0053specialize remainder_decomposition_to_mod_eq (x1)
  54. 0054specialize remainder_decomposition_to_mod_eq (x2)
  55. 0055apply remainder_decomposition_to_mod_eq
  56. 0056trans M*x1+x2
  57. 0057exact hd_witness_witness_left
  58. 0058congr
  59. 0059apply mul_comm
  60. 0060refl
  61. 0061have hc : (ModEq(m,a · x2,b) → ModEq(M,x2,x)) ∧ (ModEq(M,x2,x) → ModEq(m,a · x2,b))
  62. 0062specialize linear_congruence_solution_class_iff_reduced_modulus (a)
  63. 0063specialize linear_congruence_solution_class_iff_reduced_modulus (m)
  64. 0064specialize linear_congruence_solution_class_iff_reduced_modulus (g)
  65. 0065specialize linear_congruence_solution_class_iff_reduced_modulus (A)
  66. 0066specialize linear_congruence_solution_class_iff_reduced_modulus (M)
  67. 0067specialize linear_congruence_solution_class_iff_reduced_modulus (b)
  68. 0068specialize linear_congruence_solution_class_iff_reduced_modulus (x)
  69. 0069specialize linear_congruence_solution_class_iff_reduced_modulus (x2)
  70. 0070apply linear_congruence_solution_class_iff_reduced_modulus
  71. 0071exact hm0
  72. 0072exact hg
  73. 0073exact ha
  74. 0074exact hm
  75. 0075exact hs_witness
  76. 0076cases hc
  77. 0077apply hc_right
  78. 0078exact he