CG0007

linear_congruence_bounded_solutions_parametrized

All solutions below the original nonzero modulus are exactly r+M*t for t<g, for an actual reduced representative r.

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

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

Definition DAG

Lt(a,b) · 10IsGCD(g,a,b) · 1ModEq(m,a,b) · 10

Actual proof prerequisites

linear_congruence_solution_class_iff_reduced_moduluslinear_congruence_bounded_residue_parametrized
Original expanded first-order statement 
forall a m g A M b r x. (~(m=0)) -> ((((exists hag_left_factor_lcc_bounded. a = g * hag_left_factor_lcc_bounded) /\ (exists hag_right_factor_lcc_bounded. m = g * hag_right_factor_lcc_bounded)) /\ forall hag_divisor_lcc_bounded. (exists hag_common_left_lcc_bounded. a = hag_divisor_lcc_bounded * hag_common_left_lcc_bounded) -> (exists hag_common_right_lcc_bounded. m = hag_divisor_lcc_bounded * hag_common_right_lcc_bounded) -> exists hag_greatest_factor_lcc_bounded. g = hag_divisor_lcc_bounded * hag_greatest_factor_lcc_bounded)) -> (a=g*A) -> (m=g*M) -> (exists lcc_gap_bounded_r. lcc_gap_bounded_r+S (r)=(M)) -> (exists hgcrt_mod_left_lcc_bounded_reference hgcrt_mod_right_lcc_bounded_reference. (a * r) + m * hgcrt_mod_left_lcc_bounded_reference = b + m * hgcrt_mod_right_lcc_bounded_reference) -> ((((((exists lcc_gap_bounded_x. lcc_gap_bounded_x+S (x)=(m)) /\ ((exists hgcrt_mod_left_lcc_bounded_sol hgcrt_mod_right_lcc_bounded_sol. (a * x) + m * hgcrt_mod_left_lcc_bounded_sol = b + m * hgcrt_mod_right_lcc_bounded_sol)))) -> (exists t. ((exists lcc_gap_bounded_parameter_bound. lcc_gap_bounded_parameter_bound+S (t)=(g)) /\ (((x)=(r)+(M)*t))))) /\ (((exists t. ((exists lcc_gap_bounded_parameter_bound. lcc_gap_bounded_parameter_bound+S (t)=(g)) /\ (((x)=(r)+(M)*t)))) -> (((exists lcc_gap_bounded_x. lcc_gap_bounded_x+S (x)=(m)) /\ ((exists hgcrt_mod_left_lcc_bounded_sol hgcrt_mod_right_lcc_bounded_sol. (a * x) + m * hgcrt_mod_left_lcc_bounded_sol = b + m * hgcrt_mod_right_lcc_bounded_sol))))))))

Complete tactic proof in conservative notation

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

57 script commands · 18 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 (2)
linear congruence solution class iff reduced moduluslinear congruence bounded residue parametrized
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 r
  8. L8
    intro x
  9. L9
    intro hm0
  10. L10
    intro hg
02Fix variables and assumptionsL11–14

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

  1. L11
    intro ha
  2. L12
    intro hm
  3. L13
    intro hr
  4. L14
    intro hs
03Establish hcL15–24

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. L15
    have hc : (ModEq(m,a · x,b) → ModEq(M,x,r)) ∧ (ModEq(M,x,r) → ModEq(m,a · x,b))Definitions: ModEq(m,a · x,b)ModEq(M,x,r)Original native command in the exact edition
  2. L16
    specialize linear_congruence_solution_class_iff_reduced_modulus (a)
  3. L17
    specialize linear_congruence_solution_class_iff_reduced_modulus (m)
  4. L18
    specialize linear_congruence_solution_class_iff_reduced_modulus (g)
  5. L19
    specialize linear_congruence_solution_class_iff_reduced_modulus (A)
  6. L20
    specialize linear_congruence_solution_class_iff_reduced_modulus (M)
  7. L21
    specialize linear_congruence_solution_class_iff_reduced_modulus (b)
  8. L22
    specialize linear_congruence_solution_class_iff_reduced_modulus (r)
  9. L23
    specialize linear_congruence_solution_class_iff_reduced_modulus (x)
  10. L24
    apply linear_congruence_solution_class_iff_reduced_modulus
04Use earlier factsL25–29

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

  1. L25
    exact hm0
  2. L26
    exact hg
  3. L27
    exact ha
  4. L28
    exact hm
  5. L29
    exact hs
05Separate the logical casesL30–30

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

  1. L30
    cases hc
06Establish hpL31–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply linear congruence bounded residue parametrized.

  1. L31
    have hp : (Lt(x,g · M) ∧ ModEq(M,x,r) → ∃ y. Lt(y,g) ∧ x = r + M · y) ∧ ((∃ y. Lt(y,g) ∧ x = r + M · y) → Lt(x,g · M) ∧ ModEq(M,x,r))Definitions: Lt(x,g · M)ModEq(M,x,r)Lt(y,g)Original native command in the exact edition
  2. L32
    specialize linear_congruence_bounded_residue_parametrized (M)
  3. L33
    specialize linear_congruence_bounded_residue_parametrized (g)
  4. L34
    specialize linear_congruence_bounded_residue_parametrized (r)
  5. L35
    specialize linear_congruence_bounded_residue_parametrized (x)
  6. L36
    apply linear_congruence_bounded_residue_parametrized
  7. L37
    exact hr
07Separate the logical casesL38–39

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

  1. L38
    cases hp
  2. L39
    split
08Fix variables and assumptionsL40–40

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

  1. L40
    intro h
09Separate the logical casesL41–41

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

  1. L41
    cases h
10Use earlier factsL42–42

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

  1. L42
    apply hp_left
11Separate the logical casesL43–43

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

  1. L43
    split
12Calculate and transport equalitiesL44–44

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

  1. L44
    rewrite <- hm
13Use earlier factsL45–47

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

  1. L45
    exact h_left
  2. L46
    apply hc_left
  3. L47
    exact h_right
14Fix variables and assumptionsL48–48

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

  1. L48
    intro h
15Establish heL49–51

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

  1. L49
    have he : Lt(x,g · M) ∧ ModEq(M,x,r)Definitions: Lt(x,g · M)ModEq(M,x,r)Original native command in the exact edition
  2. L50
    apply hp_right
  3. L51
    exact h
16Separate the logical casesL52–53

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

  1. L52
    cases he
  2. L53
    split
17Calculate and transport equalitiesL54–54

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

  1. L54
    rewrite hm
18Use earlier factsL55–57

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

  1. L55
    exact he_left
  2. L56
    apply hc_right
  3. L57
    exact he_right

Library-wide reading audit

Original defined command ledger · 57 lines
  1. 0001intro a
  2. 0002intro m
  3. 0003intro g
  4. 0004intro A
  5. 0005intro M
  6. 0006intro b
  7. 0007intro r
  8. 0008intro x
  9. 0009intro hm0
  10. 0010intro hg
  11. 0011intro ha
  12. 0012intro hm
  13. 0013intro hr
  14. 0014intro hs
  15. 0015have hc : (ModEq(m,a · x,b) → ModEq(M,x,r)) ∧ (ModEq(M,x,r) → ModEq(m,a · x,b))
  16. 0016specialize linear_congruence_solution_class_iff_reduced_modulus (a)
  17. 0017specialize linear_congruence_solution_class_iff_reduced_modulus (m)
  18. 0018specialize linear_congruence_solution_class_iff_reduced_modulus (g)
  19. 0019specialize linear_congruence_solution_class_iff_reduced_modulus (A)
  20. 0020specialize linear_congruence_solution_class_iff_reduced_modulus (M)
  21. 0021specialize linear_congruence_solution_class_iff_reduced_modulus (b)
  22. 0022specialize linear_congruence_solution_class_iff_reduced_modulus (r)
  23. 0023specialize linear_congruence_solution_class_iff_reduced_modulus (x)
  24. 0024apply linear_congruence_solution_class_iff_reduced_modulus
  25. 0025exact hm0
  26. 0026exact hg
  27. 0027exact ha
  28. 0028exact hm
  29. 0029exact hs
  30. 0030cases hc
  31. 0031have hp : (Lt(x,g · M) ∧ ModEq(M,x,r) → ∃ y. Lt(y,g) ∧ x = r + M · y) ∧ ((∃ y. Lt(y,g) ∧ x = r + M · y) → Lt(x,g · M) ∧ ModEq(M,x,r))
  32. 0032specialize linear_congruence_bounded_residue_parametrized (M)
  33. 0033specialize linear_congruence_bounded_residue_parametrized (g)
  34. 0034specialize linear_congruence_bounded_residue_parametrized (r)
  35. 0035specialize linear_congruence_bounded_residue_parametrized (x)
  36. 0036apply linear_congruence_bounded_residue_parametrized
  37. 0037exact hr
  38. 0038cases hp
  39. 0039split
  40. 0040intro h
  41. 0041cases h
  42. 0042apply hp_left
  43. 0043split
  44. 0044rewrite <- hm
  45. 0045exact h_left
  46. 0046apply hc_left
  47. 0047exact h_right
  48. 0048intro h
  49. 0049have he : Lt(x,g · M) ∧ ModEq(M,x,r)
  50. 0050apply hp_right
  51. 0051exact h
  52. 0052cases he
  53. 0053split
  54. 0054rewrite hm
  55. 0055exact he_left
  56. 0056apply hc_right
  57. 0057exact he_right