CR000C

crt_pairwise_coprime_prefix_product_is_lcm

For pairwise-coprime decoded moduli the actual finite product is exactly their universal-property 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. CRTPairwiseCoprimePrefix(b,c,l) → (∃ y. ∃ z. Beta(y,z,0,1) ∧ (Beta(y,z,l,x) ∧ (∀ n. Lt(n,l) → ∃ m. ∃ k. ∃ i. Beta(b,c,n,m) ∧ (Beta(y,z,n,k) ∧ (Beta(y,z,S n,i) ∧ i = k · m))))) → CRTPrefixLCM(b,c,l,x)

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

Definition DAG

Beta(b,c,i,x) · 5CRTPairwiseCoprimePrefix(b,c,l) · 1CRTPrefixLCM(b,c,l,M) · 1Lt(a,b) · 1

Actual proof prerequisites

crt_prefix_product_common_multiplebeta_pairwise_coprime_product_divides_common_multiple · checked external prerequisite
Original expanded first-order statement 
forall b c l x. (forall bpr_left_index_gcrt_product_lcm_pairwise bpr_right_index_gcrt_product_lcm_pairwise bpr_left_value_gcrt_product_lcm_pairwise bpr_right_value_gcrt_product_lcm_pairwise. (exists bpr_gap_gcrt_product_lcm_pairwise_left_bound. bpr_gap_gcrt_product_lcm_pairwise_left_bound + S (bpr_left_index_gcrt_product_lcm_pairwise) = l) -> (exists bpr_gap_gcrt_product_lcm_pairwise_right_bound. bpr_gap_gcrt_product_lcm_pairwise_right_bound + S (bpr_right_index_gcrt_product_lcm_pairwise) = l) -> (((exists bpr_height_gcrt_product_lcm_pairwise_left_at. bpr_height_gcrt_product_lcm_pairwise_left_at + S (bpr_left_value_gcrt_product_lcm_pairwise) = S ((S (bpr_left_index_gcrt_product_lcm_pairwise)) * c)) /\ exists bpr_quotient_gcrt_product_lcm_pairwise_left_at. b = bpr_quotient_gcrt_product_lcm_pairwise_left_at * S ((S (bpr_left_index_gcrt_product_lcm_pairwise)) * c) + (bpr_left_value_gcrt_product_lcm_pairwise))) -> (((exists bpr_height_gcrt_product_lcm_pairwise_right_at. bpr_height_gcrt_product_lcm_pairwise_right_at + S (bpr_right_value_gcrt_product_lcm_pairwise) = S ((S (bpr_right_index_gcrt_product_lcm_pairwise)) * c)) /\ exists bpr_quotient_gcrt_product_lcm_pairwise_right_at. b = bpr_quotient_gcrt_product_lcm_pairwise_right_at * S ((S (bpr_right_index_gcrt_product_lcm_pairwise)) * c) + (bpr_right_value_gcrt_product_lcm_pairwise))) -> ~(bpr_left_index_gcrt_product_lcm_pairwise = bpr_right_index_gcrt_product_lcm_pairwise) -> (forall bpr_coprime_divisor_gcrt_product_lcm_pairwise_coprime. (exists bpr_coprime_left_factor_gcrt_product_lcm_pairwise_coprime. bpr_left_value_gcrt_product_lcm_pairwise = bpr_coprime_divisor_gcrt_product_lcm_pairwise_coprime * bpr_coprime_left_factor_gcrt_product_lcm_pairwise_coprime) -> (exists bpr_coprime_right_factor_gcrt_product_lcm_pairwise_coprime. bpr_right_value_gcrt_product_lcm_pairwise = bpr_coprime_divisor_gcrt_product_lcm_pairwise_coprime * bpr_coprime_right_factor_gcrt_product_lcm_pairwise_coprime) -> bpr_coprime_divisor_gcrt_product_lcm_pairwise_coprime = 1)) -> (exists ff_u_gcrt_product_lcm_source ff_v_gcrt_product_lcm_source. ((((exists ff_h_gcrt_product_lcm_source_start. ff_h_gcrt_product_lcm_source_start + S (1) = S ((S (0)) * ff_v_gcrt_product_lcm_source)) /\ exists ff_q_gcrt_product_lcm_source_start. ff_u_gcrt_product_lcm_source = ff_q_gcrt_product_lcm_source_start * S ((S (0)) * ff_v_gcrt_product_lcm_source) + (1))) /\ ((((exists ff_h_gcrt_product_lcm_source_terminal. ff_h_gcrt_product_lcm_source_terminal + S (x) = S ((S (l)) * ff_v_gcrt_product_lcm_source)) /\ exists ff_q_gcrt_product_lcm_source_terminal. ff_u_gcrt_product_lcm_source = ff_q_gcrt_product_lcm_source_terminal * S ((S (l)) * ff_v_gcrt_product_lcm_source) + (x))) /\ forall ff_i_gcrt_product_lcm_source. (exists ff_lt_gcrt_product_lcm_source_bound. ff_lt_gcrt_product_lcm_source_bound + S ff_i_gcrt_product_lcm_source = l) -> exists ff_p_gcrt_product_lcm_source ff_r_gcrt_product_lcm_source ff_s_gcrt_product_lcm_source. ((((exists ff_h_gcrt_product_lcm_source_factor. ff_h_gcrt_product_lcm_source_factor + S (ff_p_gcrt_product_lcm_source) = S ((S (ff_i_gcrt_product_lcm_source)) * c)) /\ exists ff_q_gcrt_product_lcm_source_factor. b = ff_q_gcrt_product_lcm_source_factor * S ((S (ff_i_gcrt_product_lcm_source)) * c) + (ff_p_gcrt_product_lcm_source))) /\ ((((exists ff_h_gcrt_product_lcm_source_partial. ff_h_gcrt_product_lcm_source_partial + S (ff_r_gcrt_product_lcm_source) = S ((S (ff_i_gcrt_product_lcm_source)) * ff_v_gcrt_product_lcm_source)) /\ exists ff_q_gcrt_product_lcm_source_partial. ff_u_gcrt_product_lcm_source = ff_q_gcrt_product_lcm_source_partial * S ((S (ff_i_gcrt_product_lcm_source)) * ff_v_gcrt_product_lcm_source) + (ff_r_gcrt_product_lcm_source))) /\ ((((exists ff_h_gcrt_product_lcm_source_successor. ff_h_gcrt_product_lcm_source_successor + S (ff_s_gcrt_product_lcm_source) = S ((S (S ff_i_gcrt_product_lcm_source)) * ff_v_gcrt_product_lcm_source)) /\ exists ff_q_gcrt_product_lcm_source_successor. ff_u_gcrt_product_lcm_source = ff_q_gcrt_product_lcm_source_successor * S ((S (S ff_i_gcrt_product_lcm_source)) * ff_v_gcrt_product_lcm_source) + (ff_s_gcrt_product_lcm_source))) /\ ff_s_gcrt_product_lcm_source = ff_r_gcrt_product_lcm_source * ff_p_gcrt_product_lcm_source)))))) -> (((forall gcrt_common_index_product_lcm_result_own gcrt_common_modulus_product_lcm_result_own. (exists ff_lt_gcrt_product_lcm_result_own_bound. ff_lt_gcrt_product_lcm_result_own_bound + S gcrt_common_index_product_lcm_result_own = l) -> (((exists ff_h_gcrt_product_lcm_result_own_entry. ff_h_gcrt_product_lcm_result_own_entry + S (gcrt_common_modulus_product_lcm_result_own) = S ((S (gcrt_common_index_product_lcm_result_own)) * c)) /\ exists ff_q_gcrt_product_lcm_result_own_entry. b = ff_q_gcrt_product_lcm_result_own_entry * S ((S (gcrt_common_index_product_lcm_result_own)) * c) + (gcrt_common_modulus_product_lcm_result_own))) -> exists gcrt_common_quotient_product_lcm_result_own. x = gcrt_common_modulus_product_lcm_result_own * gcrt_common_quotient_product_lcm_result_own) /\ forall gcrt_lcm_common_product_lcm_result. (forall gcrt_common_index_product_lcm_result_other gcrt_common_modulus_product_lcm_result_other. (exists ff_lt_gcrt_product_lcm_result_other_bound. ff_lt_gcrt_product_lcm_result_other_bound + S gcrt_common_index_product_lcm_result_other = l) -> (((exists ff_h_gcrt_product_lcm_result_other_entry. ff_h_gcrt_product_lcm_result_other_entry + S (gcrt_common_modulus_product_lcm_result_other) = S ((S (gcrt_common_index_product_lcm_result_other)) * c)) /\ exists ff_q_gcrt_product_lcm_result_other_entry. b = ff_q_gcrt_product_lcm_result_other_entry * S ((S (gcrt_common_index_product_lcm_result_other)) * c) + (gcrt_common_modulus_product_lcm_result_other))) -> exists gcrt_common_quotient_product_lcm_result_other. gcrt_lcm_common_product_lcm_result = gcrt_common_modulus_product_lcm_result_other * gcrt_common_quotient_product_lcm_result_other) -> exists gcrt_lcm_quotient_product_lcm_result. gcrt_lcm_common_product_lcm_result = x * gcrt_lcm_quotient_product_lcm_result))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

24 script commands · 5 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 (1)
crt prefix product common multiple
01Fix variables and assumptionsL1–6

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 x
  5. L5
    intro hpairs
  6. L6
    intro hproduct
02Separate the logical casesL7–7

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

  1. L7
    split
03Use earlier factsL8–13

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

  1. L8
    specialize crt_prefix_product_common_multiple b
  2. L9
    specialize crt_prefix_product_common_multiple c
  3. L10
    specialize crt_prefix_product_common_multiple l
  4. L11
    specialize crt_prefix_product_common_multiple x
  5. L12
    apply crt_prefix_product_common_multiple
  6. L13
    exact hproduct
04Fix variables and assumptionsL14–15

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

  1. L14
    intro z
  2. L15
    intro hcommon
05Use earlier factsL16–24

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

  1. L16
    specialize beta_pairwise_coprime_product_divides_common_multiple b
  2. L17
    specialize beta_pairwise_coprime_product_divides_common_multiple c
  3. L18
    specialize beta_pairwise_coprime_product_divides_common_multiple l
  4. L19
    specialize beta_pairwise_coprime_product_divides_common_multiple x
  5. L20
    specialize beta_pairwise_coprime_product_divides_common_multiple z
  6. L21
    apply beta_pairwise_coprime_product_divides_common_multiple
  7. L22
    exact hpairs
  8. L23
    exact hcommon
  9. L24
    exact hproduct

Library-wide reading audit

Original defined command ledger · 24 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro x
  5. 0005intro hpairs
  6. 0006intro hproduct
  7. 0007split
  8. 0008specialize crt_prefix_product_common_multiple b
  9. 0009specialize crt_prefix_product_common_multiple c
  10. 0010specialize crt_prefix_product_common_multiple l
  11. 0011specialize crt_prefix_product_common_multiple x
  12. 0012apply crt_prefix_product_common_multiple
  13. 0013exact hproduct
  14. 0014intro z
  15. 0015intro hcommon
  16. 0016specialize beta_pairwise_coprime_product_divides_common_multiple b
  17. 0017specialize beta_pairwise_coprime_product_divides_common_multiple c
  18. 0018specialize beta_pairwise_coprime_product_divides_common_multiple l
  19. 0019specialize beta_pairwise_coprime_product_divides_common_multiple x
  20. 0020specialize beta_pairwise_coprime_product_divides_common_multiple z
  21. 0021apply beta_pairwise_coprime_product_divides_common_multiple
  22. 0022exact hpairs
  23. 0023exact hcommon
  24. 0024exact hproduct