CG0004

linear_congruence_progression_bound_iff

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

With an actual remainder r<M, r+M*t is below g*M exactly when t<g; no field or coprimality hypothesis is used.

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 t. (exists lcc_gap_progression_remainder. lcc_gap_progression_remainder+S (r)=(M)) -> ((((exists lcc_gap_progression_small. lcc_gap_progression_small+S (r+M*t)=(g*M)) -> (exists lcc_gap_progression_index. lcc_gap_progression_index+S (t)=(g))) /\ (((exists lcc_gap_progression_index. lcc_gap_progression_index+S (t)=(g)) -> (exists lcc_gap_progression_small. lcc_gap_progression_small+S (r+M*t)=(g*M))))))

Constructive proof overview

Generated structural guide

With an actual remainder r<M, r+M*t is below g*M exactly when t<g; no field or coprimality hypothesis is used.

The unchanged tactic script uses 11 declared prerequisites and contains 62 exact native proof lines.

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

Proof neighborhood

Direct dependencies

le_or_lt Alpha theorem; checked-use authorized lt_not_le Alpha theorem; checked-use authorized le_trans Alpha theorem; checked-use authorized mul_le_mul_right Alpha theorem; checked-use authorized mul_comm Alpha theorem; checked-use authorized le_add_left Alpha theorem; checked-use authorized finite_add_lt_of_lt_of_le Alpha theorem; checked-use authorized le_refl Alpha theorem; checked-use authorized add_comm Alpha theorem; checked-use authorized mul_succ_left Alpha theorem; checked-use authorized lt_of_lt_of_le Alpha theorem; checked-use authorized

Direct dependents

CG0005 linear_congruence_bounded_residue_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

62 script commands · 13 reading checkpoints · 4 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.

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 t
  5. L5
    intro hr
02Separate the logical casesL6–6

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

  1. L6
    split
03Fix variables and assumptionsL7–7

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

  1. L7
    intro hb
04Establish hoL8–11

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

  1. L8
    have ho : (exists lcc_gap_progression_order. lcc_gap_progression_order+(g)=(t)) \/ (exists lcc_gap_progression_index. lcc_gap_progression_index+S (t)=(g))
  2. L9
    specialize le_or_lt (g)
  3. L10
    specialize le_or_lt (t)
  4. L11
    apply le_or_lt
05Separate the logical casesL12–13

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

  1. L12
    cases ho
  2. L13
    exfalso
06Use earlier factsL14–23

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

  1. L14
    specialize lt_not_le (r+M*t)
  2. L15
    specialize lt_not_le (g*M)
  3. L16
    apply lt_not_le
  4. L17
    exact hb
  5. L18
    specialize le_trans (g*M)
  6. L19
    specialize le_trans (t*M)
  7. L20
    specialize le_trans (r+M*t)
  8. L21
    apply le_trans
  9. L22
    specialize mul_le_mul_right (g)
  10. L23
    specialize mul_le_mul_right (t)
07Use earlier factsL24–26

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

  1. L24
    specialize mul_le_mul_right (M)
  2. L25
    apply mul_le_mul_right
  3. L26
    exact ho_left
08Establish heL27–34

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

  1. L27
    have he : t*M=M*t
  2. L28
    apply mul_comm
  3. L29
    rewrite he
  4. L30
    specialize le_add_left (M*t)
  5. L31
    specialize le_add_left (r)
  6. L32
    apply le_add_left
  7. L33
    exact ho_right
  8. L34
    intro ht
09Establish hsL35–42

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

  1. L35
    have hs : exists lcc_gap_progression_next. lcc_gap_progression_next+S (r+M*t)=(M+M*t)
  2. L36
    specialize finite_add_lt_of_lt_of_le (r)
  3. L37
    specialize finite_add_lt_of_lt_of_le (M)
  4. L38
    specialize finite_add_lt_of_lt_of_le (M*t)
  5. L39
    specialize finite_add_lt_of_lt_of_le (M*t)
  6. L40
    apply finite_add_lt_of_lt_of_le
  7. L41
    exact hr
  8. L42
    apply le_refl
10Establish heL43–52

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

  1. L43
    have he : M+M*t=S t*M
  2. L44
    trans M*t+M
  3. L45
    apply add_comm
  4. L46
    trans t*M+M
  5. L47
    congr
  6. L48
    apply mul_comm
  7. L49
    refl
  8. L50
    symm
  9. L51
    apply mul_succ_left
  10. L52
    specialize lt_of_lt_of_le (r+M*t)
11Use earlier factsL53–56

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

  1. L53
    specialize lt_of_lt_of_le (M+M*t)
  2. L54
    specialize lt_of_lt_of_le (g*M)
  3. L55
    apply lt_of_lt_of_le
  4. L56
    exact hs
12Calculate and transport equalitiesL57–57

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

  1. L57
    rewrite he
13Use earlier factsL58–62

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

  1. L58
    specialize mul_le_mul_right (S t)
  2. L59
    specialize mul_le_mul_right (g)
  3. L60
    specialize mul_le_mul_right (M)
  4. L61
    apply mul_le_mul_right
  5. L62
    exact ht

Library-wide reading audit

Original exact command ledger · 62 lines
  1. 0001intro M
  2. 0002intro g
  3. 0003intro r
  4. 0004intro t
  5. 0005intro hr
  6. 0006split
  7. 0007intro hb
  8. 0008have ho : (exists lcc_gap_progression_order. lcc_gap_progression_order+(g)=(t)) \/ (exists lcc_gap_progression_index. lcc_gap_progression_index+S (t)=(g))
  9. 0009specialize le_or_lt (g)
  10. 0010specialize le_or_lt (t)
  11. 0011apply le_or_lt
  12. 0012cases ho
  13. 0013exfalso
  14. 0014specialize lt_not_le (r+M*t)
  15. 0015specialize lt_not_le (g*M)
  16. 0016apply lt_not_le
  17. 0017exact hb
  18. 0018specialize le_trans (g*M)
  19. 0019specialize le_trans (t*M)
  20. 0020specialize le_trans (r+M*t)
  21. 0021apply le_trans
  22. 0022specialize mul_le_mul_right (g)
  23. 0023specialize mul_le_mul_right (t)
  24. 0024specialize mul_le_mul_right (M)
  25. 0025apply mul_le_mul_right
  26. 0026exact ho_left
  27. 0027have he : t*M=M*t
  28. 0028apply mul_comm
  29. 0029rewrite he
  30. 0030specialize le_add_left (M*t)
  31. 0031specialize le_add_left (r)
  32. 0032apply le_add_left
  33. 0033exact ho_right
  34. 0034intro ht
  35. 0035have hs : exists lcc_gap_progression_next. lcc_gap_progression_next+S (r+M*t)=(M+M*t)
  36. 0036specialize finite_add_lt_of_lt_of_le (r)
  37. 0037specialize finite_add_lt_of_lt_of_le (M)
  38. 0038specialize finite_add_lt_of_lt_of_le (M*t)
  39. 0039specialize finite_add_lt_of_lt_of_le (M*t)
  40. 0040apply finite_add_lt_of_lt_of_le
  41. 0041exact hr
  42. 0042apply le_refl
  43. 0043have he : M+M*t=S t*M
  44. 0044trans M*t+M
  45. 0045apply add_comm
  46. 0046trans t*M+M
  47. 0047congr
  48. 0048apply mul_comm
  49. 0049refl
  50. 0050symm
  51. 0051apply mul_succ_left
  52. 0052specialize lt_of_lt_of_le (r+M*t)
  53. 0053specialize lt_of_lt_of_le (M+M*t)
  54. 0054specialize lt_of_lt_of_le (g*M)
  55. 0055apply lt_of_lt_of_le
  56. 0056exact hs
  57. 0057rewrite he
  58. 0058specialize mul_le_mul_right (S t)
  59. 0059specialize mul_le_mul_right (g)
  60. 0060specialize mul_le_mul_right (M)
  61. 0061apply mul_le_mul_right
  62. 0062exact ht