CG0007

linear_congruence_bounded_solutions_parametrized

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 57 exact native proof lines.

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

Proof neighborhood

Direct dependencies

CG0002 linear_congruence_solution_class_iff_reduced_modulus CG0005 linear_congruence_bounded_residue_parametrized

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

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.

Named ingredients (2)
linear congruence solution class iff reduced moduluslinear congruence bounded residue parametrized

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 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
  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: LtModEq
  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 : ((exists lcc_gap_bounded_back. lcc_gap_bounded_back+S (x)=(g*M)) /\ ((exists hgcrt_mod_left_lcc_bounded_red hgcrt_mod_right_lcc_bounded_red. x + M * hgcrt_mod_left_lcc_bounded_red = r + M * hgcrt_mod_right_lcc_bounded_red)))
  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 exact 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 : (((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 hgcrt_mod_left_lcc_bounded_red hgcrt_mod_right_lcc_bounded_red. x + M * hgcrt_mod_left_lcc_bounded_red = r + M * hgcrt_mod_right_lcc_bounded_red)) /\ (((exists hgcrt_mod_left_lcc_bounded_red hgcrt_mod_right_lcc_bounded_red. x + M * hgcrt_mod_left_lcc_bounded_red = r + M * hgcrt_mod_right_lcc_bounded_red) -> (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))))
  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 : (((((exists lcc_gap_bounded_p. lcc_gap_bounded_p+S (x)=(g*M)) /\ ((exists hgcrt_mod_left_lcc_bounded_red hgcrt_mod_right_lcc_bounded_red. x + M * hgcrt_mod_left_lcc_bounded_red = r + M * hgcrt_mod_right_lcc_bounded_red)))) -> (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_p. lcc_gap_bounded_p+S (x)=(g*M)) /\ ((exists hgcrt_mod_left_lcc_bounded_red hgcrt_mod_right_lcc_bounded_red. x + M * hgcrt_mod_left_lcc_bounded_red = r + M * hgcrt_mod_right_lcc_bounded_red)))))))
  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 : ((exists lcc_gap_bounded_back. lcc_gap_bounded_back+S (x)=(g*M)) /\ ((exists hgcrt_mod_left_lcc_bounded_red hgcrt_mod_right_lcc_bounded_red. x + M * hgcrt_mod_left_lcc_bounded_red = r + M * hgcrt_mod_right_lcc_bounded_red)))
  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