CG0004

linear_congruence_progression_bound_iff

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

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. ∀ t. Lt(r,M) → (Lt(r + M · t,g · M) → Lt(t,g)) ∧ (Lt(t,g) → Lt(r + M · t,g · M))

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

Definition DAG

Le(a,b) · 1Lt(a,b) · 7

Actual proof prerequisites

le_or_lt · checked external prerequisitelt_not_le · checked external prerequisitele_trans · checked external prerequisitemul_le_mul_right · checked external prerequisitemul_comm · checked external prerequisitele_add_left · checked external prerequisitefinite_add_lt_of_lt_of_le · checked external prerequisitele_refl · checked external prerequisiteadd_comm · checked external prerequisitemul_succ_left · checked external prerequisitelt_of_lt_of_le · checked external prerequisite
Original expanded first-order 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))))))

Complete tactic proof in conservative notation

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : Le(g,t) ∨ Lt(t,g)Definitions: Le(g,t)Lt(t,g)Original native command in the exact edition
  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 : Lt(r + M · t,M + M · t)Definitions: Lt(r + M · t,M + M · t)Original native command in the exact edition
  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 defined 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 : Le(g,t) ∨ Lt(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 : Lt(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