CG0005

linear_congruence_bounded_residue_parametrized

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

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

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

Constructive proof overview

Generated structural guide

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

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

le_zero Alpha theorem; checked-use authorized succ_ne_zero Alpha theorem; checked-use authorized mod_eq_to_remainder_decomposition Alpha theorem; checked-use authorized add_comm Alpha theorem; checked-use authorized mul_comm Alpha theorem; checked-use authorized CG0004 linear_congruence_progression_bound_iff remainder_decomposition_to_mod_eq Alpha theorem; checked-use authorized

Direct dependents

CG0007 linear_congruence_bounded_solutions_parametrized

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 · 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.

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
    have hbad : exists lcc_gap_residue_bad. lcc_gap_residue_bad+S (r)=(0)
  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 : (((exists lcc_gap_residue_forward. lcc_gap_residue_forward+S (r+M*x1)=(g*M)) -> (exists lcc_gap_residue_forward_index. lcc_gap_residue_forward_index+S (x1)=(g))) /\ (((exists lcc_gap_residue_forward_index. lcc_gap_residue_forward_index+S (x1)=(g)) -> (exists lcc_gap_residue_forward. lcc_gap_residue_forward+S (r+M*x1)=(g*M)))))
  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 : (((exists lcc_gap_residue_backward. lcc_gap_residue_backward+S (r+M*x1)=(g*M)) -> (exists lcc_gap_residue_backward_index. lcc_gap_residue_backward_index+S (x1)=(g))) /\ (((exists lcc_gap_residue_backward_index. lcc_gap_residue_backward_index+S (x1)=(g)) -> (exists lcc_gap_residue_backward. lcc_gap_residue_backward+S (r+M*x1)=(g*M)))))
  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 exact 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 : exists lcc_gap_residue_bad. lcc_gap_residue_bad+S (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 : (((exists lcc_gap_residue_forward. lcc_gap_residue_forward+S (r+M*x1)=(g*M)) -> (exists lcc_gap_residue_forward_index. lcc_gap_residue_forward_index+S (x1)=(g))) /\ (((exists lcc_gap_residue_forward_index. lcc_gap_residue_forward_index+S (x1)=(g)) -> (exists lcc_gap_residue_forward. lcc_gap_residue_forward+S (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 : (((exists lcc_gap_residue_backward. lcc_gap_residue_backward+S (r+M*x1)=(g*M)) -> (exists lcc_gap_residue_backward_index. lcc_gap_residue_backward_index+S (x1)=(g))) /\ (((exists lcc_gap_residue_backward_index. lcc_gap_residue_backward_index+S (x1)=(g)) -> (exists lcc_gap_residue_backward. lcc_gap_residue_backward+S (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