CG0008

linear_congruence_exact_bounded_enumeration_exists

Construct r and an actual bijection from t<g to all solutions x<m. This is a cardinality witness, not a claimed beta-coded list.

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) ∧ ((∀ y. (Lt(y,m) ∧ ModEq(m,a · y,b) → ∃ z. Lt(z,g) ∧ y = x + M · z) ∧ ((∃ z. Lt(z,g) ∧ y = x + M · z) → Lt(y,m) ∧ ModEq(m,a · y,b))) ∧ (∀ y. ∀ z. Lt(y,g) → Lt(z,g) → x + M · y = x + M · z → y = z)))

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

Definition DAG

Lt(a,b) · 8Dvd(d,n) · 1IsGCD(g,a,b) · 1ModEq(m,a,b) · 4

Actual proof prerequisites

mul_zero_left · checked external prerequisitelinear_congruence_reduced_representative_existslinear_congruence_bounded_solutions_parametrizedlinear_congruence_bounded_parameter_unique
Original expanded first-order statement 
forall a m g A M b. (~(m=0)) -> ((((exists hag_left_factor_lcc_enumeration. a = g * hag_left_factor_lcc_enumeration) /\ (exists hag_right_factor_lcc_enumeration. m = g * hag_right_factor_lcc_enumeration)) /\ forall hag_divisor_lcc_enumeration. (exists hag_common_left_lcc_enumeration. a = hag_divisor_lcc_enumeration * hag_common_left_lcc_enumeration) -> (exists hag_common_right_lcc_enumeration. m = hag_divisor_lcc_enumeration * hag_common_right_lcc_enumeration) -> exists hag_greatest_factor_lcc_enumeration. g = hag_divisor_lcc_enumeration * hag_greatest_factor_lcc_enumeration)) -> (a=g*A) -> (m=g*M) -> (exists lcc_enum_bfactor. b=g*lcc_enum_bfactor) -> (exists r. ((exists lcc_gap_enumeration_r. lcc_gap_enumeration_r+S (r)=(M)) /\ (((exists hgcrt_mod_left_lcc_enumeration_reference hgcrt_mod_right_lcc_enumeration_reference. (a * r) + m * hgcrt_mod_left_lcc_enumeration_reference = b + m * hgcrt_mod_right_lcc_enumeration_reference) /\ (((forall x. (((((exists lcc_gap_enumeration_x. lcc_gap_enumeration_x+S (x)=(m)) /\ ((exists hgcrt_mod_left_lcc_enumeration_solution hgcrt_mod_right_lcc_enumeration_solution. (a * x) + m * hgcrt_mod_left_lcc_enumeration_solution = b + m * hgcrt_mod_right_lcc_enumeration_solution)))) -> (exists t. ((exists lcc_gap_enumeration_param_bound. lcc_gap_enumeration_param_bound+S (t)=(g)) /\ (((x)=(r)+(M)*t))))) /\ (((exists t. ((exists lcc_gap_enumeration_param_bound. lcc_gap_enumeration_param_bound+S (t)=(g)) /\ (((x)=(r)+(M)*t)))) -> (((exists lcc_gap_enumeration_x. lcc_gap_enumeration_x+S (x)=(m)) /\ ((exists hgcrt_mod_left_lcc_enumeration_solution hgcrt_mod_right_lcc_enumeration_solution. (a * x) + m * hgcrt_mod_left_lcc_enumeration_solution = b + m * hgcrt_mod_right_lcc_enumeration_solution)))))))) /\ ((forall t u. (exists lcc_gap_enumeration_t. lcc_gap_enumeration_t+S (t)=(g)) -> (exists lcc_gap_enumeration_u. lcc_gap_enumeration_u+S (u)=(g)) -> ((r)+M*t=(r)+M*u) -> t=u))))))))

Complete tactic proof in conservative notation

All 76 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

76 script commands · 20 reading checkpoints · 3 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 (3)
linear congruence reduced representative existslinear congruence bounded solutions parametrizedlinear congruence bounded parameter unique
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 hrL26–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply linear congruence reduced representative exists.

  1. L26
    have hr : ∃ r. Lt(r,M) ∧ ModEq(m,a · r,b)Definitions: Lt(r,M)ModEq(m,a · r,b)Original native command in the exact edition
  2. L27
    specialize linear_congruence_reduced_representative_exists (a)
  3. L28
    specialize linear_congruence_reduced_representative_exists (m)
  4. L29
    specialize linear_congruence_reduced_representative_exists (g)
  5. L30
    specialize linear_congruence_reduced_representative_exists (A)
  6. L31
    specialize linear_congruence_reduced_representative_exists (M)
  7. L32
    specialize linear_congruence_reduced_representative_exists (b)
  8. L33
    apply linear_congruence_reduced_representative_exists
  9. L34
    exact hm0
  10. L35
    exact hg
06Use earlier factsL36–38

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

  1. L36
    exact ha
  2. L37
    exact hm
  3. L38
    exact hb
07Separate the logical casesL39–40

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

  1. L39
    cases hr
  2. L40
    cases hr_witness
08Construct an explicit witnessL41–41

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

  1. L41
    exists x
09Separate the logical casesL42–42

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

  1. L42
    split
10Use earlier factsL43–43

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

  1. L43
    exact hr_witness_left
11Separate the logical casesL44–44

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

  1. L44
    split
12Use earlier factsL45–45

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

  1. L45
    exact hr_witness_right
13Separate the logical casesL46–46

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

  1. L46
    split
14Fix variables and assumptionsL47–47

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

  1. L47
    intro y
15Use earlier factsL48–57

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

  1. L48
    specialize linear_congruence_bounded_solutions_parametrized (a)
  2. L49
    specialize linear_congruence_bounded_solutions_parametrized (m)
  3. L50
    specialize linear_congruence_bounded_solutions_parametrized (g)
  4. L51
    specialize linear_congruence_bounded_solutions_parametrized (A)
  5. L52
    specialize linear_congruence_bounded_solutions_parametrized (M)
  6. L53
    specialize linear_congruence_bounded_solutions_parametrized (b)
  7. L54
    specialize linear_congruence_bounded_solutions_parametrized (x)
  8. L55
    specialize linear_congruence_bounded_solutions_parametrized (y)
  9. L56
    apply linear_congruence_bounded_solutions_parametrized
  10. L57
    exact hm0
16Use earlier factsL58–62

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

  1. L58
    exact hg
  2. L59
    exact ha
  3. L60
    exact hm
  4. L61
    exact hr_witness_left
  5. L62
    exact hr_witness_right
17Fix variables and assumptionsL63–67

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

  1. L63
    intro t
  2. L64
    intro u
  3. L65
    intro ht
  4. L66
    intro hu
  5. L67
    intro he
18Use earlier factsL68–74

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

  1. L68
    specialize linear_congruence_bounded_parameter_unique (M)
  2. L69
    specialize linear_congruence_bounded_parameter_unique (x)
  3. L70
    specialize linear_congruence_bounded_parameter_unique (x+M*t)
  4. L71
    specialize linear_congruence_bounded_parameter_unique (t)
  5. L72
    specialize linear_congruence_bounded_parameter_unique (u)
  6. L73
    apply linear_congruence_bounded_parameter_unique
  7. L74
    exact hM0
19Calculate and transport equalitiesL75–75

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

  1. L75
    refl
20Use earlier factsL76–76

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

  1. L76
    exact he

Library-wide reading audit

Original defined command ledger · 76 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 hr : ∃ r. Lt(r,M) ∧ ModEq(m,a · r,b)
  27. 0027specialize linear_congruence_reduced_representative_exists (a)
  28. 0028specialize linear_congruence_reduced_representative_exists (m)
  29. 0029specialize linear_congruence_reduced_representative_exists (g)
  30. 0030specialize linear_congruence_reduced_representative_exists (A)
  31. 0031specialize linear_congruence_reduced_representative_exists (M)
  32. 0032specialize linear_congruence_reduced_representative_exists (b)
  33. 0033apply linear_congruence_reduced_representative_exists
  34. 0034exact hm0
  35. 0035exact hg
  36. 0036exact ha
  37. 0037exact hm
  38. 0038exact hb
  39. 0039cases hr
  40. 0040cases hr_witness
  41. 0041exists x
  42. 0042split
  43. 0043exact hr_witness_left
  44. 0044split
  45. 0045exact hr_witness_right
  46. 0046split
  47. 0047intro y
  48. 0048specialize linear_congruence_bounded_solutions_parametrized (a)
  49. 0049specialize linear_congruence_bounded_solutions_parametrized (m)
  50. 0050specialize linear_congruence_bounded_solutions_parametrized (g)
  51. 0051specialize linear_congruence_bounded_solutions_parametrized (A)
  52. 0052specialize linear_congruence_bounded_solutions_parametrized (M)
  53. 0053specialize linear_congruence_bounded_solutions_parametrized (b)
  54. 0054specialize linear_congruence_bounded_solutions_parametrized (x)
  55. 0055specialize linear_congruence_bounded_solutions_parametrized (y)
  56. 0056apply linear_congruence_bounded_solutions_parametrized
  57. 0057exact hm0
  58. 0058exact hg
  59. 0059exact ha
  60. 0060exact hm
  61. 0061exact hr_witness_left
  62. 0062exact hr_witness_right
  63. 0063intro t
  64. 0064intro u
  65. 0065intro ht
  66. 0066intro hu
  67. 0067intro he
  68. 0068specialize linear_congruence_bounded_parameter_unique (M)
  69. 0069specialize linear_congruence_bounded_parameter_unique (x)
  70. 0070specialize linear_congruence_bounded_parameter_unique (x+M*t)
  71. 0071specialize linear_congruence_bounded_parameter_unique (t)
  72. 0072specialize linear_congruence_bounded_parameter_unique (u)
  73. 0073apply linear_congruence_bounded_parameter_unique
  74. 0074exact hM0
  75. 0075refl
  76. 0076exact he