CR0010

crt_prefix_lcm_exists_unique

Every arbitrary finite decoded modulus list, including noncoprime and zero entries, has a unique exact lcm.

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. ∃ x. CRTPrefixLCM(b,c,l,x) ∧ (∀ y. CRTPrefixLCM(b,c,l,y) → y = x)

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

Definition DAG

CRTPrefixLCM(b,c,l,M) · 2

Actual proof prerequisites

crt_prefix_lcm_emptycrt_prefix_lcm_uniquebeta_at_exists · checked external prerequisitelcm_exists_relational · checked external prerequisitecrt_prefix_lcm_successor_intro
Original expanded first-order statement 
forall b c l. exists x. ((((forall gcrt_common_index_general_lcm_chosen_own gcrt_common_modulus_general_lcm_chosen_own. (exists ff_lt_gcrt_general_lcm_chosen_own_bound. ff_lt_gcrt_general_lcm_chosen_own_bound + S gcrt_common_index_general_lcm_chosen_own = l) -> (((exists ff_h_gcrt_general_lcm_chosen_own_entry. ff_h_gcrt_general_lcm_chosen_own_entry + S (gcrt_common_modulus_general_lcm_chosen_own) = S ((S (gcrt_common_index_general_lcm_chosen_own)) * c)) /\ exists ff_q_gcrt_general_lcm_chosen_own_entry. b = ff_q_gcrt_general_lcm_chosen_own_entry * S ((S (gcrt_common_index_general_lcm_chosen_own)) * c) + (gcrt_common_modulus_general_lcm_chosen_own))) -> exists gcrt_common_quotient_general_lcm_chosen_own. x = gcrt_common_modulus_general_lcm_chosen_own * gcrt_common_quotient_general_lcm_chosen_own) /\ forall gcrt_lcm_common_general_lcm_chosen. (forall gcrt_common_index_general_lcm_chosen_other gcrt_common_modulus_general_lcm_chosen_other. (exists ff_lt_gcrt_general_lcm_chosen_other_bound. ff_lt_gcrt_general_lcm_chosen_other_bound + S gcrt_common_index_general_lcm_chosen_other = l) -> (((exists ff_h_gcrt_general_lcm_chosen_other_entry. ff_h_gcrt_general_lcm_chosen_other_entry + S (gcrt_common_modulus_general_lcm_chosen_other) = S ((S (gcrt_common_index_general_lcm_chosen_other)) * c)) /\ exists ff_q_gcrt_general_lcm_chosen_other_entry. b = ff_q_gcrt_general_lcm_chosen_other_entry * S ((S (gcrt_common_index_general_lcm_chosen_other)) * c) + (gcrt_common_modulus_general_lcm_chosen_other))) -> exists gcrt_common_quotient_general_lcm_chosen_other. gcrt_lcm_common_general_lcm_chosen = gcrt_common_modulus_general_lcm_chosen_other * gcrt_common_quotient_general_lcm_chosen_other) -> exists gcrt_lcm_quotient_general_lcm_chosen. gcrt_lcm_common_general_lcm_chosen = x * gcrt_lcm_quotient_general_lcm_chosen)) /\ forall y. (((forall gcrt_common_index_general_lcm_compared_own gcrt_common_modulus_general_lcm_compared_own. (exists ff_lt_gcrt_general_lcm_compared_own_bound. ff_lt_gcrt_general_lcm_compared_own_bound + S gcrt_common_index_general_lcm_compared_own = l) -> (((exists ff_h_gcrt_general_lcm_compared_own_entry. ff_h_gcrt_general_lcm_compared_own_entry + S (gcrt_common_modulus_general_lcm_compared_own) = S ((S (gcrt_common_index_general_lcm_compared_own)) * c)) /\ exists ff_q_gcrt_general_lcm_compared_own_entry. b = ff_q_gcrt_general_lcm_compared_own_entry * S ((S (gcrt_common_index_general_lcm_compared_own)) * c) + (gcrt_common_modulus_general_lcm_compared_own))) -> exists gcrt_common_quotient_general_lcm_compared_own. y = gcrt_common_modulus_general_lcm_compared_own * gcrt_common_quotient_general_lcm_compared_own) /\ forall gcrt_lcm_common_general_lcm_compared. (forall gcrt_common_index_general_lcm_compared_other gcrt_common_modulus_general_lcm_compared_other. (exists ff_lt_gcrt_general_lcm_compared_other_bound. ff_lt_gcrt_general_lcm_compared_other_bound + S gcrt_common_index_general_lcm_compared_other = l) -> (((exists ff_h_gcrt_general_lcm_compared_other_entry. ff_h_gcrt_general_lcm_compared_other_entry + S (gcrt_common_modulus_general_lcm_compared_other) = S ((S (gcrt_common_index_general_lcm_compared_other)) * c)) /\ exists ff_q_gcrt_general_lcm_compared_other_entry. b = ff_q_gcrt_general_lcm_compared_other_entry * S ((S (gcrt_common_index_general_lcm_compared_other)) * c) + (gcrt_common_modulus_general_lcm_compared_other))) -> exists gcrt_common_quotient_general_lcm_compared_other. gcrt_lcm_common_general_lcm_compared = gcrt_common_modulus_general_lcm_compared_other * gcrt_common_quotient_general_lcm_compared_other) -> exists gcrt_lcm_quotient_general_lcm_compared. gcrt_lcm_common_general_lcm_compared = y * gcrt_lcm_quotient_general_lcm_compared)) -> y = x)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

62 script commands · 18 reading checkpoints · 1 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 (3)
crt prefix lcm emptycrt prefix lcm uniquecrt prefix lcm successor intro
01Fix variables and assumptionsL1–2

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on lL3–3

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction l
03Construct an explicit witnessL4–4

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

  1. L4
    exists 1
04Separate the logical casesL5–5

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

  1. L5
    split
05Use earlier factsL6–8

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

  1. L6
    specialize crt_prefix_lcm_empty b
  2. L7
    specialize crt_prefix_lcm_empty c
  3. L8
    exact crt_prefix_lcm_empty
06Fix variables and assumptionsL9–10

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

  1. L9
    intro y
  2. L10
    intro hy
07Use earlier factsL11–20

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

  1. L11
    specialize crt_prefix_lcm_unique b
  2. L12
    specialize crt_prefix_lcm_unique c
  3. L13
    specialize crt_prefix_lcm_unique 0
  4. L14
    specialize crt_prefix_lcm_unique y
  5. L15
    specialize crt_prefix_lcm_unique 1
  6. L16
    apply crt_prefix_lcm_unique
  7. L17
    exact hy
  8. L18
    specialize crt_prefix_lcm_empty b
  9. L19
    specialize crt_prefix_lcm_empty c
  10. L20
    exact crt_prefix_lcm_empty
08Separate the logical casesL21–22

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

  1. L21
    cases IH
  2. L22
    cases IH_witness
09Establish hlastL23–27

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

  1. L23
    have hlast : exists m. (((exists ff_h_gcrt_general_lcm_last. ff_h_gcrt_general_lcm_last + S (m) = S ((S (l)) * c)) /\ exists ff_q_gcrt_general_lcm_last. b = ff_q_gcrt_general_lcm_last * S ((S (l)) * c) + (m)))
  2. L24
    specialize beta_at_exists b
  3. L25
    specialize beta_at_exists c
  4. L26
    specialize beta_at_exists l
  5. L27
    exact beta_at_exists
10Separate the logical casesL28–28

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

  1. L28
    cases hlast
11Use earlier factsL29–30

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

  1. L29
    specialize lcm_exists_relational x
  2. L30
    specialize lcm_exists_relational x1
12Separate the logical casesL31–31

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

  1. L31
    cases lcm_exists_relational
13Construct an explicit witnessL32–32

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

  1. L32
    exists x2
14Separate the logical casesL33–33

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

  1. L33
    split
15Use earlier factsL34–43

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

  1. L34
    specialize crt_prefix_lcm_successor_intro b
  2. L35
    specialize crt_prefix_lcm_successor_intro c
  3. L36
    specialize crt_prefix_lcm_successor_intro l
  4. L37
    specialize crt_prefix_lcm_successor_intro x
  5. L38
    specialize crt_prefix_lcm_successor_intro x1
  6. L39
    specialize crt_prefix_lcm_successor_intro x2
  7. L40
    apply crt_prefix_lcm_successor_intro
  8. L41
    exact IH_witness_left
  9. L42
    exact hlast_witness
  10. L43
    exact lcm_exists_relational_witness
16Fix variables and assumptionsL44–45

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

  1. L44
    intro y
  2. L45
    intro hy
17Use earlier factsL46–55

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

  1. L46
    specialize crt_prefix_lcm_unique b
  2. L47
    specialize crt_prefix_lcm_unique c
  3. L48
    specialize crt_prefix_lcm_unique (S l)
  4. L49
    specialize crt_prefix_lcm_unique y
  5. L50
    specialize crt_prefix_lcm_unique x2
  6. L51
    apply crt_prefix_lcm_unique
  7. L52
    exact hy
  8. L53
    specialize crt_prefix_lcm_successor_intro b
  9. L54
    specialize crt_prefix_lcm_successor_intro c
  10. L55
    specialize crt_prefix_lcm_successor_intro l
18Use earlier factsL56–62

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

  1. L56
    specialize crt_prefix_lcm_successor_intro x
  2. L57
    specialize crt_prefix_lcm_successor_intro x1
  3. L58
    specialize crt_prefix_lcm_successor_intro x2
  4. L59
    apply crt_prefix_lcm_successor_intro
  5. L60
    exact IH_witness_left
  6. L61
    exact hlast_witness
  7. L62
    exact lcm_exists_relational_witness

Library-wide reading audit

Original defined command ledger · 62 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004exists 1
  5. 0005split
  6. 0006specialize crt_prefix_lcm_empty b
  7. 0007specialize crt_prefix_lcm_empty c
  8. 0008exact crt_prefix_lcm_empty
  9. 0009intro y
  10. 0010intro hy
  11. 0011specialize crt_prefix_lcm_unique b
  12. 0012specialize crt_prefix_lcm_unique c
  13. 0013specialize crt_prefix_lcm_unique 0
  14. 0014specialize crt_prefix_lcm_unique y
  15. 0015specialize crt_prefix_lcm_unique 1
  16. 0016apply crt_prefix_lcm_unique
  17. 0017exact hy
  18. 0018specialize crt_prefix_lcm_empty b
  19. 0019specialize crt_prefix_lcm_empty c
  20. 0020exact crt_prefix_lcm_empty
  21. 0021cases IH
  22. 0022cases IH_witness
  23. 0023have hlast : exists m. (((exists ff_h_gcrt_general_lcm_last. ff_h_gcrt_general_lcm_last + S (m) = S ((S (l)) * c)) /\ exists ff_q_gcrt_general_lcm_last. b = ff_q_gcrt_general_lcm_last * S ((S (l)) * c) + (m)))
  24. 0024specialize beta_at_exists b
  25. 0025specialize beta_at_exists c
  26. 0026specialize beta_at_exists l
  27. 0027exact beta_at_exists
  28. 0028cases hlast
  29. 0029specialize lcm_exists_relational x
  30. 0030specialize lcm_exists_relational x1
  31. 0031cases lcm_exists_relational
  32. 0032exists x2
  33. 0033split
  34. 0034specialize crt_prefix_lcm_successor_intro b
  35. 0035specialize crt_prefix_lcm_successor_intro c
  36. 0036specialize crt_prefix_lcm_successor_intro l
  37. 0037specialize crt_prefix_lcm_successor_intro x
  38. 0038specialize crt_prefix_lcm_successor_intro x1
  39. 0039specialize crt_prefix_lcm_successor_intro x2
  40. 0040apply crt_prefix_lcm_successor_intro
  41. 0041exact IH_witness_left
  42. 0042exact hlast_witness
  43. 0043exact lcm_exists_relational_witness
  44. 0044intro y
  45. 0045intro hy
  46. 0046specialize crt_prefix_lcm_unique b
  47. 0047specialize crt_prefix_lcm_unique c
  48. 0048specialize crt_prefix_lcm_unique (S l)
  49. 0049specialize crt_prefix_lcm_unique y
  50. 0050specialize crt_prefix_lcm_unique x2
  51. 0051apply crt_prefix_lcm_unique
  52. 0052exact hy
  53. 0053specialize crt_prefix_lcm_successor_intro b
  54. 0054specialize crt_prefix_lcm_successor_intro c
  55. 0055specialize crt_prefix_lcm_successor_intro l
  56. 0056specialize crt_prefix_lcm_successor_intro x
  57. 0057specialize crt_prefix_lcm_successor_intro x1
  58. 0058specialize crt_prefix_lcm_successor_intro x2
  59. 0059apply crt_prefix_lcm_successor_intro
  60. 0060exact IH_witness_left
  61. 0061exact hlast_witness
  62. 0062exact lcm_exists_relational_witness