CG0005

linear_congruence_bounded_residue_parametrized

Construct the exact interval parameter for every bounded member of a residue class, and conversely.

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

∀ M. ∀ g. ∀ r. ∀ x. Lt(r,M) → (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))

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

Definition DAG

Lt(a,b) · 14ModEq(m,a,b) · 2

Actual proof prerequisites

le_zero · checked external prerequisitesucc_ne_zero · checked external prerequisitemod_eq_to_remainder_decomposition · checked external prerequisiteadd_comm · checked external prerequisitemul_comm · checked external prerequisitelinear_congruence_progression_bound_iffremainder_decomposition_to_mod_eq · checked external prerequisite
Original expanded first-order statement 
forall M g r x. (exists lcc_gap_residue_reference. lcc_gap_residue_reference+S (r)=(M)) -> ((((((exists lcc_gap_residue_bound. lcc_gap_residue_bound+S (x)=(g*M)) /\ ((exists hgcrt_mod_left_lcc_residue_mod hgcrt_mod_right_lcc_residue_mod. x + M * hgcrt_mod_left_lcc_residue_mod = r + M * hgcrt_mod_right_lcc_residue_mod)))) -> (exists t. ((exists lcc_gap_residue_parameter_bound. lcc_gap_residue_parameter_bound+S (t)=(g)) /\ (((x)=(r)+(M)*t))))) /\ (((exists t. ((exists lcc_gap_residue_parameter_bound. lcc_gap_residue_parameter_bound+S (t)=(g)) /\ (((x)=(r)+(M)*t)))) -> (((exists lcc_gap_residue_bound. lcc_gap_residue_bound+S (x)=(g*M)) /\ ((exists hgcrt_mod_left_lcc_residue_mod hgcrt_mod_right_lcc_residue_mod. x + M * hgcrt_mod_left_lcc_residue_mod = r + M * hgcrt_mod_right_lcc_residue_mod))))))))

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 · 30 reading checkpoints · 7 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 progression bound iff
01Fix variables and assumptionsL1–5

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

  1. L1
    intro M
  2. L2
    intro g
  3. L3
    intro r
  4. L4
    intro x
  5. L5
    intro hr
02Establish hM0L6–7

Establish this local claim before using it. It is not an additional assumption.

  1. L6
    have hM0 : ~(M=0)
  2. L7
    intro hz
03Establish hbadL8–10

Establish this local claim before using it. It is not an additional assumption.

  1. L8
  2. L9
    rewrite <- hz
  3. L10
    exact hr
04Establish hsL11–17

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

  1. L11
    have hs : S r=0
  2. L12
    specialize le_zero (S r)
  3. L13
    apply le_zero
  4. L14
    exact hbad
  5. L15
    specialize succ_ne_zero r
  6. L16
    apply succ_ne_zero
  7. L17
    exact hs
05Separate the logical casesL18–18

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

  1. L18
    split
06Fix variables and assumptionsL19–19

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

  1. L19
    intro h
07Separate the logical casesL20–20

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

  1. L20
    cases h
08Establish hqL21–28

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

  1. L21
    have hq : exists q. x=q*M+r
  2. L22
    specialize mod_eq_to_remainder_decomposition (M)
  3. L23
    specialize mod_eq_to_remainder_decomposition (x)
  4. L24
    specialize mod_eq_to_remainder_decomposition (r)
  5. L25
    apply mod_eq_to_remainder_decomposition
  6. L26
    exact hM0
  7. L27
    exact hr
  8. L28
    exact h_right
09Separate the logical casesL29–29

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

  1. L29
    cases hq
10Establish heL30–37

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

  1. L30
    have he : x=r+M*x1
  2. L31
    trans x1*M+r
  3. L32
    exact hq_witness
  4. L33
    trans r+x1*M
  5. L34
    apply add_comm
  6. L35
    congr
  7. L36
    refl
  8. L37
    apply mul_comm
11Construct an explicit witnessL38–38

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

  1. L38
    exists x1
12Separate the logical casesL39–39

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

  1. L39
    split
13Establish hcL40–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply linear congruence progression bound iff.

  1. L40
    have hc : (Lt(r + M · x1,g · M) → Lt(x1,g)) ∧ (Lt(x1,g) → Lt(r + M · x1,g · M))Definitions: Lt(r + M · x1,g · M)Lt(x1,g)Original native command in the exact edition
  2. L41
    specialize linear_congruence_progression_bound_iff (M)
  3. L42
    specialize linear_congruence_progression_bound_iff (g)
  4. L43
    specialize linear_congruence_progression_bound_iff (r)
  5. L44
    specialize linear_congruence_progression_bound_iff (x1)
  6. L45
    apply linear_congruence_progression_bound_iff
  7. L46
    exact hr
14Separate the logical casesL47–47

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

  1. L47
    cases hc
15Use earlier factsL48–48

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

  1. L48
    apply hc_left
16Calculate and transport equalitiesL49–49

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

  1. L49
    rewrite <- he
17Use earlier factsL50–51

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

  1. L50
    exact h_left
  2. L51
    exact he
18Fix variables and assumptionsL52–52

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

  1. L52
    intro h
19Separate the logical casesL53–55

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

  1. L53
    cases h
  2. L54
    cases h_witness
  3. L55
    split
20Calculate and transport equalitiesL56–56

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

  1. L56
    rewrite h_witness_right
21Establish hcL57–63

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply linear congruence progression bound iff.

  1. L57
    have hc : (Lt(r + M · x1,g · M) → Lt(x1,g)) ∧ (Lt(x1,g) → Lt(r + M · x1,g · M))Definitions: Lt(r + M · x1,g · M)Lt(x1,g)Original native command in the exact edition
  2. L58
    specialize linear_congruence_progression_bound_iff (M)
  3. L59
    specialize linear_congruence_progression_bound_iff (g)
  4. L60
    specialize linear_congruence_progression_bound_iff (r)
  5. L61
    specialize linear_congruence_progression_bound_iff (x1)
  6. L62
    apply linear_congruence_progression_bound_iff
  7. L63
    exact hr
22Separate the logical casesL64–64

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

  1. L64
    cases hc
23Use earlier factsL65–71

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

  1. L65
    apply hc_right
  2. L66
    exact h_witness_left
  3. L67
    specialize remainder_decomposition_to_mod_eq (M)
  4. L68
    specialize remainder_decomposition_to_mod_eq (x)
  5. L69
    specialize remainder_decomposition_to_mod_eq (x1)
  6. L70
    specialize remainder_decomposition_to_mod_eq (r)
  7. L71
    apply remainder_decomposition_to_mod_eq
24Calculate and transport equalitiesL72–72

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

  1. L72
    trans r+M*x1
25Use earlier factsL73–73

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

  1. L73
    exact h_witness_right
26Calculate and transport equalitiesL74–74

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

  1. L74
    trans M*x1+r
27Use earlier factsL75–75

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

  1. L75
    apply add_comm
28Calculate and transport equalitiesL76–76

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

  1. L76
    congr
29Use earlier factsL77–77

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

  1. L77
    apply mul_comm
30Calculate and transport equalitiesL78–78

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

  1. L78
    refl

Library-wide reading audit

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