CR000F

crt_prefix_lcm_successor_intro

Binary relational lcm extends the exact universal-property lcm of any finite decoded modulus prefix.

Alpha v34 checked-use · first admitted v24 · 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. Exact original first-admission records.

Historical partial components only: this chapter proves canonical solutions for finite positive pairwise-coprime systems and exact LCM solution classes. G011 is now closed in the separate Alpha-v27 generalized-crt branch for arbitrary pairwise-compatible systems, including noncoprime moduli. Full G011 proof · Alpha v27

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ l. ∀ P. ∀ m. ∀ M. CRTPrefixLCM(b,c,l,P) → Beta(b,c,l,m) → Dvd(P,M) ∧ Dvd(m,M) ∧ (∀ x. Dvd(P,x) → Dvd(m,x) → Dvd(M,x)) → CRTPrefixLCM(b,c,S l,M)

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

Definition DAG

Beta(b,c,i,x) · 1CRTPrefixLCM(b,c,l,M) · 2Dvd(d,n) · 5

Actual proof prerequisites

finite_lt_succ_eq_or_lt · checked external prerequisitebeta_at_unique · checked external prerequisiteis_lcm_multiple_left · checked external prerequisiteis_lcm_multiple_right · checked external prerequisitemultiple_trans · checked external prerequisiteis_lcm_least · checked external prerequisitele_succ · checked external prerequisitele_refl · checked external prerequisite
Original expanded first-order statement 
forall b c l P m M. (((forall gcrt_common_index_step_prefix_lcm_own gcrt_common_modulus_step_prefix_lcm_own. (exists ff_lt_gcrt_step_prefix_lcm_own_bound. ff_lt_gcrt_step_prefix_lcm_own_bound + S gcrt_common_index_step_prefix_lcm_own = l) -> (((exists ff_h_gcrt_step_prefix_lcm_own_entry. ff_h_gcrt_step_prefix_lcm_own_entry + S (gcrt_common_modulus_step_prefix_lcm_own) = S ((S (gcrt_common_index_step_prefix_lcm_own)) * c)) /\ exists ff_q_gcrt_step_prefix_lcm_own_entry. b = ff_q_gcrt_step_prefix_lcm_own_entry * S ((S (gcrt_common_index_step_prefix_lcm_own)) * c) + (gcrt_common_modulus_step_prefix_lcm_own))) -> exists gcrt_common_quotient_step_prefix_lcm_own. P = gcrt_common_modulus_step_prefix_lcm_own * gcrt_common_quotient_step_prefix_lcm_own) /\ forall gcrt_lcm_common_step_prefix_lcm. (forall gcrt_common_index_step_prefix_lcm_other gcrt_common_modulus_step_prefix_lcm_other. (exists ff_lt_gcrt_step_prefix_lcm_other_bound. ff_lt_gcrt_step_prefix_lcm_other_bound + S gcrt_common_index_step_prefix_lcm_other = l) -> (((exists ff_h_gcrt_step_prefix_lcm_other_entry. ff_h_gcrt_step_prefix_lcm_other_entry + S (gcrt_common_modulus_step_prefix_lcm_other) = S ((S (gcrt_common_index_step_prefix_lcm_other)) * c)) /\ exists ff_q_gcrt_step_prefix_lcm_other_entry. b = ff_q_gcrt_step_prefix_lcm_other_entry * S ((S (gcrt_common_index_step_prefix_lcm_other)) * c) + (gcrt_common_modulus_step_prefix_lcm_other))) -> exists gcrt_common_quotient_step_prefix_lcm_other. gcrt_lcm_common_step_prefix_lcm = gcrt_common_modulus_step_prefix_lcm_other * gcrt_common_quotient_step_prefix_lcm_other) -> exists gcrt_lcm_quotient_step_prefix_lcm. gcrt_lcm_common_step_prefix_lcm = P * gcrt_lcm_quotient_step_prefix_lcm)) -> (((exists ff_h_gcrt_step_last_modulus. ff_h_gcrt_step_last_modulus + S (m) = S ((S (l)) * c)) /\ exists ff_q_gcrt_step_last_modulus. b = ff_q_gcrt_step_last_modulus * S ((S (l)) * c) + (m))) -> ((((exists hlcm_left_factor_gcrt_step_binary_lcm. M = P * hlcm_left_factor_gcrt_step_binary_lcm) /\ (exists hlcm_right_factor_gcrt_step_binary_lcm. M = m * hlcm_right_factor_gcrt_step_binary_lcm)) /\ forall hlcm_common_gcrt_step_binary_lcm. (exists hlcm_left_common_gcrt_step_binary_lcm. hlcm_common_gcrt_step_binary_lcm = P * hlcm_left_common_gcrt_step_binary_lcm) -> (exists hlcm_right_common_gcrt_step_binary_lcm. hlcm_common_gcrt_step_binary_lcm = m * hlcm_right_common_gcrt_step_binary_lcm) -> exists hlcm_least_factor_gcrt_step_binary_lcm. hlcm_common_gcrt_step_binary_lcm = M * hlcm_least_factor_gcrt_step_binary_lcm)) -> (((forall gcrt_common_index_step_result_lcm_own gcrt_common_modulus_step_result_lcm_own. (exists ff_lt_gcrt_step_result_lcm_own_bound. ff_lt_gcrt_step_result_lcm_own_bound + S gcrt_common_index_step_result_lcm_own = S l) -> (((exists ff_h_gcrt_step_result_lcm_own_entry. ff_h_gcrt_step_result_lcm_own_entry + S (gcrt_common_modulus_step_result_lcm_own) = S ((S (gcrt_common_index_step_result_lcm_own)) * c)) /\ exists ff_q_gcrt_step_result_lcm_own_entry. b = ff_q_gcrt_step_result_lcm_own_entry * S ((S (gcrt_common_index_step_result_lcm_own)) * c) + (gcrt_common_modulus_step_result_lcm_own))) -> exists gcrt_common_quotient_step_result_lcm_own. M = gcrt_common_modulus_step_result_lcm_own * gcrt_common_quotient_step_result_lcm_own) /\ forall gcrt_lcm_common_step_result_lcm. (forall gcrt_common_index_step_result_lcm_other gcrt_common_modulus_step_result_lcm_other. (exists ff_lt_gcrt_step_result_lcm_other_bound. ff_lt_gcrt_step_result_lcm_other_bound + S gcrt_common_index_step_result_lcm_other = S l) -> (((exists ff_h_gcrt_step_result_lcm_other_entry. ff_h_gcrt_step_result_lcm_other_entry + S (gcrt_common_modulus_step_result_lcm_other) = S ((S (gcrt_common_index_step_result_lcm_other)) * c)) /\ exists ff_q_gcrt_step_result_lcm_other_entry. b = ff_q_gcrt_step_result_lcm_other_entry * S ((S (gcrt_common_index_step_result_lcm_other)) * c) + (gcrt_common_modulus_step_result_lcm_other))) -> exists gcrt_common_quotient_step_result_lcm_other. gcrt_lcm_common_step_result_lcm = gcrt_common_modulus_step_result_lcm_other * gcrt_common_quotient_step_result_lcm_other) -> exists gcrt_lcm_quotient_step_result_lcm. gcrt_lcm_common_step_result_lcm = M * gcrt_lcm_quotient_step_result_lcm))

Complete unchanged native tactic proof

All 80 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

80 script commands · 14 reading checkpoints · 2 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–9

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro P
  5. L5
    intro m
  6. L6
    intro M
  7. L7
    intro hprefix
  8. L8
    intro hm
  9. L9
    intro hbinary
02Separate the logical casesL10–11

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

  1. L10
    cases hprefix
  2. L11
    split
03Fix variables and assumptionsL12–15

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

  1. L12
    intro i
  2. L13
    intro n
  3. L14
    intro hi
  4. L15
    intro hn
04Establish hsplitL16–20

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

  1. L16
    have hsplit : i = l \/ exists gap. gap + S i = l
  2. L17
    specialize finite_lt_succ_eq_or_lt l
  3. L18
    specialize finite_lt_succ_eq_or_lt i
  4. L19
    apply finite_lt_succ_eq_or_lt
  5. L20
    exact hi
05Separate the logical casesL21–21

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

  1. L21
    cases hsplit
06Calculate and transport equalitiesL22–23

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

  1. L22
    rewrite hsplit_left at hn
  2. L23
    rewrite hsplit_left at hn
07Establish heqL24–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L24
    have heq : n = m
  2. L25
    specialize beta_at_unique b
  3. L26
    specialize beta_at_unique c
  4. L27
    specialize beta_at_unique l
  5. L28
    specialize beta_at_unique n
  6. L29
    specialize beta_at_unique m
  7. L30
    apply beta_at_unique
  8. L31
    exact hn
  9. L32
    exact hm
  10. L33
    rewrite heq
08Use earlier factsL34–43

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

  1. L34
    specialize is_lcm_multiple_right M
  2. L35
    specialize is_lcm_multiple_right P
  3. L36
    specialize is_lcm_multiple_right m
  4. L37
    apply is_lcm_multiple_right
  5. L38
    exact hbinary
  6. L39
    specialize multiple_trans P
  7. L40
    specialize multiple_trans n
  8. L41
    specialize multiple_trans M
  9. L42
    apply multiple_trans
  10. L43
    specialize is_lcm_multiple_left M
09Use earlier factsL44–52

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

  1. L44
    specialize is_lcm_multiple_left P
  2. L45
    specialize is_lcm_multiple_left m
  3. L46
    apply is_lcm_multiple_left
  4. L47
    exact hbinary
  5. L48
    specialize hprefix_left i
  6. L49
    specialize hprefix_left n
  7. L50
    apply hprefix_left
  8. L51
    exact hsplit_right
  9. L52
    exact hn
10Fix variables and assumptionsL53–54

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

  1. L53
    intro z
  2. L54
    intro hcommon
11Use earlier factsL55–62

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

  1. L55
    specialize is_lcm_least M
  2. L56
    specialize is_lcm_least P
  3. L57
    specialize is_lcm_least m
  4. L58
    specialize is_lcm_least z
  5. L59
    apply is_lcm_least
  6. L60
    exact hbinary
  7. L61
    specialize hprefix_right z
  8. L62
    apply hprefix_right
12Fix variables and assumptionsL63–66

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

  1. L63
    intro i
  2. L64
    intro n
  3. L65
    intro hi
  4. L66
    intro hn
13Use earlier factsL67–76

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

  1. L67
    specialize hcommon i
  2. L68
    specialize hcommon n
  3. L69
    apply hcommon
  4. L70
    specialize le_succ (S i)
  5. L71
    specialize le_succ l
  6. L72
    apply le_succ
  7. L73
    exact hi
  8. L74
    exact hn
  9. L75
    specialize hcommon l
  10. L76
    specialize hcommon m
14Use earlier factsL77–80

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

  1. L77
    apply hcommon
  2. L78
    specialize le_refl (S l)
  3. L79
    exact le_refl
  4. L80
    exact hm

Library-wide reading audit

Original defined command ledger · 80 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro P
  5. 0005intro m
  6. 0006intro M
  7. 0007intro hprefix
  8. 0008intro hm
  9. 0009intro hbinary
  10. 0010cases hprefix
  11. 0011split
  12. 0012intro i
  13. 0013intro n
  14. 0014intro hi
  15. 0015intro hn
  16. 0016have hsplit : i = l \/ exists gap. gap + S i = l
  17. 0017specialize finite_lt_succ_eq_or_lt l
  18. 0018specialize finite_lt_succ_eq_or_lt i
  19. 0019apply finite_lt_succ_eq_or_lt
  20. 0020exact hi
  21. 0021cases hsplit
  22. 0022rewrite hsplit_left at hn
  23. 0023rewrite hsplit_left at hn
  24. 0024have heq : n = m
  25. 0025specialize beta_at_unique b
  26. 0026specialize beta_at_unique c
  27. 0027specialize beta_at_unique l
  28. 0028specialize beta_at_unique n
  29. 0029specialize beta_at_unique m
  30. 0030apply beta_at_unique
  31. 0031exact hn
  32. 0032exact hm
  33. 0033rewrite heq
  34. 0034specialize is_lcm_multiple_right M
  35. 0035specialize is_lcm_multiple_right P
  36. 0036specialize is_lcm_multiple_right m
  37. 0037apply is_lcm_multiple_right
  38. 0038exact hbinary
  39. 0039specialize multiple_trans P
  40. 0040specialize multiple_trans n
  41. 0041specialize multiple_trans M
  42. 0042apply multiple_trans
  43. 0043specialize is_lcm_multiple_left M
  44. 0044specialize is_lcm_multiple_left P
  45. 0045specialize is_lcm_multiple_left m
  46. 0046apply is_lcm_multiple_left
  47. 0047exact hbinary
  48. 0048specialize hprefix_left i
  49. 0049specialize hprefix_left n
  50. 0050apply hprefix_left
  51. 0051exact hsplit_right
  52. 0052exact hn
  53. 0053intro z
  54. 0054intro hcommon
  55. 0055specialize is_lcm_least M
  56. 0056specialize is_lcm_least P
  57. 0057specialize is_lcm_least m
  58. 0058specialize is_lcm_least z
  59. 0059apply is_lcm_least
  60. 0060exact hbinary
  61. 0061specialize hprefix_right z
  62. 0062apply hprefix_right
  63. 0063intro i
  64. 0064intro n
  65. 0065intro hi
  66. 0066intro hn
  67. 0067specialize hcommon i
  68. 0068specialize hcommon n
  69. 0069apply hcommon
  70. 0070specialize le_succ (S i)
  71. 0071specialize le_succ l
  72. 0072apply le_succ
  73. 0073exact hi
  74. 0074exact hn
  75. 0075specialize hcommon l
  76. 0076specialize hcommon m
  77. 0077apply hcommon
  78. 0078specialize le_refl (S l)
  79. 0079exact le_refl
  80. 0080exact hm