CG0003

linear_congruence_reduced_representative_exists

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

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

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 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))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 7 declared prerequisites and contains 78 exact native proof lines.

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

Proof neighborhood

Direct dependencies

mul_zero_left Alpha theorem; checked-use authorized linear_congruence_gcd_divisibility_constructs_solution Alpha theorem; checked-use authorized division_remainder_exists Alpha theorem; checked-use authorized mod_eq_symm Alpha theorem; checked-use authorized remainder_decomposition_to_mod_eq Alpha theorem; checked-use authorized mul_comm Alpha theorem; checked-use authorized CG0002 linear_congruence_solution_class_iff_reduced_modulus

Direct dependents

CG0008 linear_congruence_exact_bounded_enumeration_exists

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

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.

Named ingredients (1)
linear congruence solution class iff reduced modulus

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 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 : exists x. exists hgcrt_mod_left_lcc_representative_original hgcrt_mod_right_lcc_representative_original. (a * x) + m * hgcrt_mod_left_lcc_representative_original = b + m * hgcrt_mod_right_lcc_representative_original
  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 : exists q r. ((x=M*q+r) /\ ((exists lcc_gap_representative_division. lcc_gap_representative_division+S (r)=(M))))
  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
    have he : exists hgcrt_mod_left_lcc_representative_equal hgcrt_mod_right_lcc_representative_equal. x2 + M * hgcrt_mod_left_lcc_representative_equal = x + M * hgcrt_mod_right_lcc_representative_equal
  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
  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 exact 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 : exists x. exists hgcrt_mod_left_lcc_representative_original hgcrt_mod_right_lcc_representative_original. (a * x) + m * hgcrt_mod_left_lcc_representative_original = b + m * hgcrt_mod_right_lcc_representative_original
  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 : exists q r. ((x=M*q+r) /\ ((exists lcc_gap_representative_division. lcc_gap_representative_division+S (r)=(M))))
  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 : exists hgcrt_mod_left_lcc_representative_equal hgcrt_mod_right_lcc_representative_equal. x2 + M * hgcrt_mod_left_lcc_representative_equal = x + M * hgcrt_mod_right_lcc_representative_equal
  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 : (((exists hgcrt_mod_left_lcc_representative_target hgcrt_mod_right_lcc_representative_target. (a * x2) + m * hgcrt_mod_left_lcc_representative_target = b + m * hgcrt_mod_right_lcc_representative_target) -> (exists hgcrt_mod_left_lcc_representative_class hgcrt_mod_right_lcc_representative_class. x2 + M * hgcrt_mod_left_lcc_representative_class = x + M * hgcrt_mod_right_lcc_representative_class)) /\ (((exists hgcrt_mod_left_lcc_representative_class hgcrt_mod_right_lcc_representative_class. x2 + M * hgcrt_mod_left_lcc_representative_class = x + M * hgcrt_mod_right_lcc_representative_class) -> (exists hgcrt_mod_left_lcc_representative_target hgcrt_mod_right_lcc_representative_target. (a * x2) + m * hgcrt_mod_left_lcc_representative_target = b + m * hgcrt_mod_right_lcc_representative_target))))
  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