CR0011

crt_pairwise_coprime_prefix_lcm_exists_unique

Every arbitrary finite pairwise-coprime modulus list has a unique relational 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. CRTPairwiseCoprimePrefix(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

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

Actual proof prerequisites

beta_product_exists_unique · checked external prerequisitecrt_pairwise_coprime_prefix_product_is_lcmcrt_prefix_lcm_unique
Original expanded first-order statement 
forall b c l. (forall bpr_left_index_gcrt_lcm_exists_pairwise bpr_right_index_gcrt_lcm_exists_pairwise bpr_left_value_gcrt_lcm_exists_pairwise bpr_right_value_gcrt_lcm_exists_pairwise. (exists bpr_gap_gcrt_lcm_exists_pairwise_left_bound. bpr_gap_gcrt_lcm_exists_pairwise_left_bound + S (bpr_left_index_gcrt_lcm_exists_pairwise) = l) -> (exists bpr_gap_gcrt_lcm_exists_pairwise_right_bound. bpr_gap_gcrt_lcm_exists_pairwise_right_bound + S (bpr_right_index_gcrt_lcm_exists_pairwise) = l) -> (((exists bpr_height_gcrt_lcm_exists_pairwise_left_at. bpr_height_gcrt_lcm_exists_pairwise_left_at + S (bpr_left_value_gcrt_lcm_exists_pairwise) = S ((S (bpr_left_index_gcrt_lcm_exists_pairwise)) * c)) /\ exists bpr_quotient_gcrt_lcm_exists_pairwise_left_at. b = bpr_quotient_gcrt_lcm_exists_pairwise_left_at * S ((S (bpr_left_index_gcrt_lcm_exists_pairwise)) * c) + (bpr_left_value_gcrt_lcm_exists_pairwise))) -> (((exists bpr_height_gcrt_lcm_exists_pairwise_right_at. bpr_height_gcrt_lcm_exists_pairwise_right_at + S (bpr_right_value_gcrt_lcm_exists_pairwise) = S ((S (bpr_right_index_gcrt_lcm_exists_pairwise)) * c)) /\ exists bpr_quotient_gcrt_lcm_exists_pairwise_right_at. b = bpr_quotient_gcrt_lcm_exists_pairwise_right_at * S ((S (bpr_right_index_gcrt_lcm_exists_pairwise)) * c) + (bpr_right_value_gcrt_lcm_exists_pairwise))) -> ~(bpr_left_index_gcrt_lcm_exists_pairwise = bpr_right_index_gcrt_lcm_exists_pairwise) -> (forall bpr_coprime_divisor_gcrt_lcm_exists_pairwise_coprime. (exists bpr_coprime_left_factor_gcrt_lcm_exists_pairwise_coprime. bpr_left_value_gcrt_lcm_exists_pairwise = bpr_coprime_divisor_gcrt_lcm_exists_pairwise_coprime * bpr_coprime_left_factor_gcrt_lcm_exists_pairwise_coprime) -> (exists bpr_coprime_right_factor_gcrt_lcm_exists_pairwise_coprime. bpr_right_value_gcrt_lcm_exists_pairwise = bpr_coprime_divisor_gcrt_lcm_exists_pairwise_coprime * bpr_coprime_right_factor_gcrt_lcm_exists_pairwise_coprime) -> bpr_coprime_divisor_gcrt_lcm_exists_pairwise_coprime = 1)) -> exists x. ((((forall gcrt_common_index_lcm_exists_chosen_own gcrt_common_modulus_lcm_exists_chosen_own. (exists ff_lt_gcrt_lcm_exists_chosen_own_bound. ff_lt_gcrt_lcm_exists_chosen_own_bound + S gcrt_common_index_lcm_exists_chosen_own = l) -> (((exists ff_h_gcrt_lcm_exists_chosen_own_entry. ff_h_gcrt_lcm_exists_chosen_own_entry + S (gcrt_common_modulus_lcm_exists_chosen_own) = S ((S (gcrt_common_index_lcm_exists_chosen_own)) * c)) /\ exists ff_q_gcrt_lcm_exists_chosen_own_entry. b = ff_q_gcrt_lcm_exists_chosen_own_entry * S ((S (gcrt_common_index_lcm_exists_chosen_own)) * c) + (gcrt_common_modulus_lcm_exists_chosen_own))) -> exists gcrt_common_quotient_lcm_exists_chosen_own. x = gcrt_common_modulus_lcm_exists_chosen_own * gcrt_common_quotient_lcm_exists_chosen_own) /\ forall gcrt_lcm_common_lcm_exists_chosen. (forall gcrt_common_index_lcm_exists_chosen_other gcrt_common_modulus_lcm_exists_chosen_other. (exists ff_lt_gcrt_lcm_exists_chosen_other_bound. ff_lt_gcrt_lcm_exists_chosen_other_bound + S gcrt_common_index_lcm_exists_chosen_other = l) -> (((exists ff_h_gcrt_lcm_exists_chosen_other_entry. ff_h_gcrt_lcm_exists_chosen_other_entry + S (gcrt_common_modulus_lcm_exists_chosen_other) = S ((S (gcrt_common_index_lcm_exists_chosen_other)) * c)) /\ exists ff_q_gcrt_lcm_exists_chosen_other_entry. b = ff_q_gcrt_lcm_exists_chosen_other_entry * S ((S (gcrt_common_index_lcm_exists_chosen_other)) * c) + (gcrt_common_modulus_lcm_exists_chosen_other))) -> exists gcrt_common_quotient_lcm_exists_chosen_other. gcrt_lcm_common_lcm_exists_chosen = gcrt_common_modulus_lcm_exists_chosen_other * gcrt_common_quotient_lcm_exists_chosen_other) -> exists gcrt_lcm_quotient_lcm_exists_chosen. gcrt_lcm_common_lcm_exists_chosen = x * gcrt_lcm_quotient_lcm_exists_chosen)) /\ forall y. (((forall gcrt_common_index_lcm_exists_compared_own gcrt_common_modulus_lcm_exists_compared_own. (exists ff_lt_gcrt_lcm_exists_compared_own_bound. ff_lt_gcrt_lcm_exists_compared_own_bound + S gcrt_common_index_lcm_exists_compared_own = l) -> (((exists ff_h_gcrt_lcm_exists_compared_own_entry. ff_h_gcrt_lcm_exists_compared_own_entry + S (gcrt_common_modulus_lcm_exists_compared_own) = S ((S (gcrt_common_index_lcm_exists_compared_own)) * c)) /\ exists ff_q_gcrt_lcm_exists_compared_own_entry. b = ff_q_gcrt_lcm_exists_compared_own_entry * S ((S (gcrt_common_index_lcm_exists_compared_own)) * c) + (gcrt_common_modulus_lcm_exists_compared_own))) -> exists gcrt_common_quotient_lcm_exists_compared_own. y = gcrt_common_modulus_lcm_exists_compared_own * gcrt_common_quotient_lcm_exists_compared_own) /\ forall gcrt_lcm_common_lcm_exists_compared. (forall gcrt_common_index_lcm_exists_compared_other gcrt_common_modulus_lcm_exists_compared_other. (exists ff_lt_gcrt_lcm_exists_compared_other_bound. ff_lt_gcrt_lcm_exists_compared_other_bound + S gcrt_common_index_lcm_exists_compared_other = l) -> (((exists ff_h_gcrt_lcm_exists_compared_other_entry. ff_h_gcrt_lcm_exists_compared_other_entry + S (gcrt_common_modulus_lcm_exists_compared_other) = S ((S (gcrt_common_index_lcm_exists_compared_other)) * c)) /\ exists ff_q_gcrt_lcm_exists_compared_other_entry. b = ff_q_gcrt_lcm_exists_compared_other_entry * S ((S (gcrt_common_index_lcm_exists_compared_other)) * c) + (gcrt_common_modulus_lcm_exists_compared_other))) -> exists gcrt_common_quotient_lcm_exists_compared_other. gcrt_lcm_common_lcm_exists_compared = gcrt_common_modulus_lcm_exists_compared_other * gcrt_common_quotient_lcm_exists_compared_other) -> exists gcrt_lcm_quotient_lcm_exists_compared. gcrt_lcm_common_lcm_exists_compared = y * gcrt_lcm_quotient_lcm_exists_compared)) -> y = x)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

34 script commands · 9 reading checkpoints · 0 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 (2)
crt pairwise coprime prefix product is lcmcrt prefix lcm unique
01Fix variables and assumptionsL1–4

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 hpairs
02Use earlier factsL5–7

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

  1. L5
    specialize beta_product_exists_unique b
  2. L6
    specialize beta_product_exists_unique c
  3. L7
    specialize beta_product_exists_unique l
03Separate the logical casesL8–9

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

  1. L8
    cases beta_product_exists_unique
  2. L9
    cases beta_product_exists_unique_witness
04Construct an explicit witnessL10–10

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

  1. L10
    exists x
05Separate the logical casesL11–11

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

  1. L11
    split
06Use earlier factsL12–18

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

  1. L12
    specialize crt_pairwise_coprime_prefix_product_is_lcm b
  2. L13
    specialize crt_pairwise_coprime_prefix_product_is_lcm c
  3. L14
    specialize crt_pairwise_coprime_prefix_product_is_lcm l
  4. L15
    specialize crt_pairwise_coprime_prefix_product_is_lcm x
  5. L16
    apply crt_pairwise_coprime_prefix_product_is_lcm
  6. L17
    exact hpairs
  7. L18
    exact beta_product_exists_unique_witness_left
07Fix variables and assumptionsL19–20

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

  1. L19
    intro y
  2. L20
    intro hy
08Use earlier factsL21–30

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

  1. L21
    specialize crt_prefix_lcm_unique b
  2. L22
    specialize crt_prefix_lcm_unique c
  3. L23
    specialize crt_prefix_lcm_unique l
  4. L24
    specialize crt_prefix_lcm_unique y
  5. L25
    specialize crt_prefix_lcm_unique x
  6. L26
    apply crt_prefix_lcm_unique
  7. L27
    exact hy
  8. L28
    specialize crt_pairwise_coprime_prefix_product_is_lcm b
  9. L29
    specialize crt_pairwise_coprime_prefix_product_is_lcm c
  10. L30
    specialize crt_pairwise_coprime_prefix_product_is_lcm l
09Use earlier factsL31–34

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

  1. L31
    specialize crt_pairwise_coprime_prefix_product_is_lcm x
  2. L32
    apply crt_pairwise_coprime_prefix_product_is_lcm
  3. L33
    exact hpairs
  4. L34
    exact beta_product_exists_unique_witness_left

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro hpairs
  5. 0005specialize beta_product_exists_unique b
  6. 0006specialize beta_product_exists_unique c
  7. 0007specialize beta_product_exists_unique l
  8. 0008cases beta_product_exists_unique
  9. 0009cases beta_product_exists_unique_witness
  10. 0010exists x
  11. 0011split
  12. 0012specialize crt_pairwise_coprime_prefix_product_is_lcm b
  13. 0013specialize crt_pairwise_coprime_prefix_product_is_lcm c
  14. 0014specialize crt_pairwise_coprime_prefix_product_is_lcm l
  15. 0015specialize crt_pairwise_coprime_prefix_product_is_lcm x
  16. 0016apply crt_pairwise_coprime_prefix_product_is_lcm
  17. 0017exact hpairs
  18. 0018exact beta_product_exists_unique_witness_left
  19. 0019intro y
  20. 0020intro hy
  21. 0021specialize crt_prefix_lcm_unique b
  22. 0022specialize crt_prefix_lcm_unique c
  23. 0023specialize crt_prefix_lcm_unique l
  24. 0024specialize crt_prefix_lcm_unique y
  25. 0025specialize crt_prefix_lcm_unique x
  26. 0026apply crt_prefix_lcm_unique
  27. 0027exact hy
  28. 0028specialize crt_pairwise_coprime_prefix_product_is_lcm b
  29. 0029specialize crt_pairwise_coprime_prefix_product_is_lcm c
  30. 0030specialize crt_pairwise_coprime_prefix_product_is_lcm l
  31. 0031specialize crt_pairwise_coprime_prefix_product_is_lcm x
  32. 0032apply crt_pairwise_coprime_prefix_product_is_lcm
  33. 0033exact hpairs
  34. 0034exact beta_product_exists_unique_witness_left