FC000D — crt_pairwise_compatible_prefix_implies_merge_compatible

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.

All finite lists are included, even the empty list and zero moduli. A positive LCM gives x<M; at zero LCM congruence is exact equality and normalization deliberately does not require the impossible x<0.

Exact theorem in conservative defined notation

∀ r. ∀ s. ∀ b. ∀ c. ∀ l. CRTPairwiseCompatiblePrefix(r,s,b,c,l) → ∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. Lt(x,l) → CRTPrefixLCM(b,c,x,z) → CRTPrefixSolution(r,s,b,c,x,y) → BetaAt(r,s,x,n) → BetaAt(b,c,x,m) → IsGCD(k,z,m) → ModEq(k,y,n)

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

Definition DAG

CRTPrefixSolution(r,s,b,c,l,x) · 1 CRTPrefixLCM(b,c,l,M) · 1 CRTPairwiseCompatiblePrefix(r,s,b,c,l) · 1 Lt(a,b) · 1 IsGCD(g,a,b) · 1 ModEq(m,a,b) · 1 BetaAt(b,c,i,x) · 2

Actual proof prerequisites

crt_prefix_gcd_congruences_lcm crt_pairwise_compatible_prefix_induces_gcd_congruences

Original expanded first-order statement

forall r s b c l. (forall gcomp_left_index_gfull_full_pairs_source gcomp_right_index_gfull_full_pairs_source gcomp_left_residue_gfull_full_pairs_source gcomp_right_residue_gfull_full_pairs_source gcomp_left_modulus_gfull_full_pairs_source gcomp_right_modulus_gfull_full_pairs_source gcomp_pair_gcd_gfull_full_pairs_source. (exists ff_lt_gcrt_gfull_full_pairs_source_left_bound. ff_lt_gcrt_gfull_full_pairs_source_left_bound + S gcomp_left_index_gfull_full_pairs_source = l) -> (exists ff_lt_gcrt_gfull_full_pairs_source_right_bound. ff_lt_gcrt_gfull_full_pairs_source_right_bound + S gcomp_right_index_gfull_full_pairs_source = l) -> (((exists ff_h_gcrt_gfull_full_pairs_source_left_residue. ff_h_gcrt_gfull_full_pairs_source_left_residue + S (gcomp_left_residue_gfull_full_pairs_source) = S ((S (gcomp_left_index_gfull_full_pairs_source)) * s)) /\ exists ff_q_gcrt_gfull_full_pairs_source_left_residue. r = ff_q_gcrt_gfull_full_pairs_source_left_residue * S ((S (gcomp_left_index_gfull_full_pairs_source)) * s) + (gcomp_left_residue_gfull_full_pairs_source))) -> (((exists ff_h_gcrt_gfull_full_pairs_source_right_residue. ff_h_gcrt_gfull_full_pairs_source_right_residue + S (gcomp_right_residue_gfull_full_pairs_source) = S ((S (gcomp_right_index_gfull_full_pairs_source)) * s)) /\ exists ff_q_gcrt_gfull_full_pairs_source_right_residue. r = ff_q_gcrt_gfull_full_pairs_source_right_residue * S ((S (gcomp_right_index_gfull_full_pairs_source)) * s) + (gcomp_right_residue_gfull_full_pairs_source))) -> (((exists ff_h_gcrt_gfull_full_pairs_source_left_modulus. ff_h_gcrt_gfull_full_pairs_source_left_modulus + S (gcomp_left_modulus_gfull_full_pairs_source) = S ((S (gcomp_left_index_gfull_full_pairs_source)) * c)) /\ exists ff_q_gcrt_gfull_full_pairs_source_left_modulus. b = ff_q_gcrt_gfull_full_pairs_source_left_modulus * S ((S (gcomp_left_index_gfull_full_pairs_source)) * c) + (gcomp_left_modulus_gfull_full_pairs_source))) -> (((exists ff_h_gcrt_gfull_full_pairs_source_right_modulus. ff_h_gcrt_gfull_full_pairs_source_right_modulus + S (gcomp_right_modulus_gfull_full_pairs_source) = S ((S (gcomp_right_index_gfull_full_pairs_source)) * c)) /\ exists ff_q_gcrt_gfull_full_pairs_source_right_modulus. b = ff_q_gcrt_gfull_full_pairs_source_right_modulus * S ((S (gcomp_right_index_gfull_full_pairs_source)) * c) + (gcomp_right_modulus_gfull_full_pairs_source))) -> ((((exists hag_left_factor_gcomp_gfull_full_pairs_source_gcd. gcomp_left_modulus_gfull_full_pairs_source = gcomp_pair_gcd_gfull_full_pairs_source * hag_left_factor_gcomp_gfull_full_pairs_source_gcd) /\ (exists hag_right_factor_gcomp_gfull_full_pairs_source_gcd. gcomp_right_modulus_gfull_full_pairs_source = gcomp_pair_gcd_gfull_full_pairs_source * hag_right_factor_gcomp_gfull_full_pairs_source_gcd)) /\ forall hag_divisor_gcomp_gfull_full_pairs_source_gcd. (exists hag_common_left_gcomp_gfull_full_pairs_source_gcd. gcomp_left_modulus_gfull_full_pairs_source = hag_divisor_gcomp_gfull_full_pairs_source_gcd * hag_common_left_gcomp_gfull_full_pairs_source_gcd) -> (exists hag_common_right_gcomp_gfull_full_pairs_source_gcd. gcomp_right_modulus_gfull_full_pairs_source = hag_divisor_gcomp_gfull_full_pairs_source_gcd * hag_common_right_gcomp_gfull_full_pairs_source_gcd) -> exists hag_greatest_factor_gcomp_gfull_full_pairs_source_gcd. gcomp_pair_gcd_gfull_full_pairs_source = hag_divisor_gcomp_gfull_full_pairs_source_gcd * hag_greatest_factor_gcomp_gfull_full_pairs_source_gcd)) -> (exists hgcrt_mod_left_gcrt_gfull_full_pairs_source_result hgcrt_mod_right_gcrt_gfull_full_pairs_source_result. gcomp_left_residue_gfull_full_pairs_source + gcomp_pair_gcd_gfull_full_pairs_source * hgcrt_mod_left_gcrt_gfull_full_pairs_source_result = gcomp_right_residue_gfull_full_pairs_source + gcomp_pair_gcd_gfull_full_pairs_source * hgcrt_mod_right_gcrt_gfull_full_pairs_source_result)) -> (forall gcomp_merge_index_gfull_full_merge_result gcomp_merge_solution_gfull_full_merge_result gcomp_merge_lcm_gfull_full_merge_result gcomp_merge_residue_gfull_full_merge_result gcomp_merge_modulus_gfull_full_merge_result gcomp_merge_gcd_gfull_full_merge_result. (exists ff_lt_gcrt_gfull_full_merge_result_bound. ff_lt_gcrt_gfull_full_merge_result_bound + S gcomp_merge_index_gfull_full_merge_result = l) -> (((forall gcrt_common_index_gfull_full_merge_result_lcm_own gcrt_common_modulus_gfull_full_merge_result_lcm_own. (exists ff_lt_gcrt_gfull_full_merge_result_lcm_own_bound. ff_lt_gcrt_gfull_full_merge_result_lcm_own_bound + S gcrt_common_index_gfull_full_merge_result_lcm_own = gcomp_merge_index_gfull_full_merge_result) -> (((exists ff_h_gcrt_gfull_full_merge_result_lcm_own_entry. ff_h_gcrt_gfull_full_merge_result_lcm_own_entry + S (gcrt_common_modulus_gfull_full_merge_result_lcm_own) = S ((S (gcrt_common_index_gfull_full_merge_result_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_full_merge_result_lcm_own_entry. b = ff_q_gcrt_gfull_full_merge_result_lcm_own_entry * S ((S (gcrt_common_index_gfull_full_merge_result_lcm_own)) * c) + (gcrt_common_modulus_gfull_full_merge_result_lcm_own))) -> exists gcrt_common_quotient_gfull_full_merge_result_lcm_own. gcomp_merge_lcm_gfull_full_merge_result = gcrt_common_modulus_gfull_full_merge_result_lcm_own * gcrt_common_quotient_gfull_full_merge_result_lcm_own) /\ forall gcrt_lcm_common_gfull_full_merge_result_lcm. (forall gcrt_common_index_gfull_full_merge_result_lcm_other gcrt_common_modulus_gfull_full_merge_result_lcm_other. (exists ff_lt_gcrt_gfull_full_merge_result_lcm_other_bound. ff_lt_gcrt_gfull_full_merge_result_lcm_other_bound + S gcrt_common_index_gfull_full_merge_result_lcm_other = gcomp_merge_index_gfull_full_merge_result) -> (((exists ff_h_gcrt_gfull_full_merge_result_lcm_other_entry. ff_h_gcrt_gfull_full_merge_result_lcm_other_entry + S (gcrt_common_modulus_gfull_full_merge_result_lcm_other) = S ((S (gcrt_common_index_gfull_full_merge_result_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_full_merge_result_lcm_other_entry. b = ff_q_gcrt_gfull_full_merge_result_lcm_other_entry * S ((S (gcrt_common_index_gfull_full_merge_result_lcm_other)) * c) + (gcrt_common_modulus_gfull_full_merge_result_lcm_other))) -> exists gcrt_common_quotient_gfull_full_merge_result_lcm_other. gcrt_lcm_common_gfull_full_merge_result_lcm = gcrt_common_modulus_gfull_full_merge_result_lcm_other * gcrt_common_quotient_gfull_full_merge_result_lcm_other) -> exists gcrt_lcm_quotient_gfull_full_merge_result_lcm. gcrt_lcm_common_gfull_full_merge_result_lcm = gcomp_merge_lcm_gfull_full_merge_result * gcrt_lcm_quotient_gfull_full_merge_result_lcm)) -> (forall gcrt_solution_index_gfull_full_merge_result_solution gcrt_solution_residue_gfull_full_merge_result_solution gcrt_solution_modulus_gfull_full_merge_result_solution. (exists ff_lt_gcrt_gfull_full_merge_result_solution_bound. ff_lt_gcrt_gfull_full_merge_result_solution_bound + S gcrt_solution_index_gfull_full_merge_result_solution = gcomp_merge_index_gfull_full_merge_result) -> (((exists ff_h_gcrt_gfull_full_merge_result_solution_residue. ff_h_gcrt_gfull_full_merge_result_solution_residue + S (gcrt_solution_residue_gfull_full_merge_result_solution) = S ((S (gcrt_solution_index_gfull_full_merge_result_solution)) * s)) /\ exists ff_q_gcrt_gfull_full_merge_result_solution_residue. r = ff_q_gcrt_gfull_full_merge_result_solution_residue * S ((S (gcrt_solution_index_gfull_full_merge_result_solution)) * s) + (gcrt_solution_residue_gfull_full_merge_result_solution))) -> (((exists ff_h_gcrt_gfull_full_merge_result_solution_modulus. ff_h_gcrt_gfull_full_merge_result_solution_modulus + S (gcrt_solution_modulus_gfull_full_merge_result_solution) = S ((S (gcrt_solution_index_gfull_full_merge_result_solution)) * c)) /\ exists ff_q_gcrt_gfull_full_merge_result_solution_modulus. b = ff_q_gcrt_gfull_full_merge_result_solution_modulus * S ((S (gcrt_solution_index_gfull_full_merge_result_solution)) * c) + (gcrt_solution_modulus_gfull_full_merge_result_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_full_merge_result_solution_congruence hgcrt_mod_right_gcrt_gfull_full_merge_result_solution_congruence. gcomp_merge_solution_gfull_full_merge_result + gcrt_solution_modulus_gfull_full_merge_result_solution * hgcrt_mod_left_gcrt_gfull_full_merge_result_solution_congruence = gcrt_solution_residue_gfull_full_merge_result_solution + gcrt_solution_modulus_gfull_full_merge_result_solution * hgcrt_mod_right_gcrt_gfull_full_merge_result_solution_congruence)) -> (((exists ff_h_gcrt_gfull_full_merge_result_residue. ff_h_gcrt_gfull_full_merge_result_residue + S (gcomp_merge_residue_gfull_full_merge_result) = S ((S (gcomp_merge_index_gfull_full_merge_result)) * s)) /\ exists ff_q_gcrt_gfull_full_merge_result_residue. r = ff_q_gcrt_gfull_full_merge_result_residue * S ((S (gcomp_merge_index_gfull_full_merge_result)) * s) + (gcomp_merge_residue_gfull_full_merge_result))) -> (((exists ff_h_gcrt_gfull_full_merge_result_modulus. ff_h_gcrt_gfull_full_merge_result_modulus + S (gcomp_merge_modulus_gfull_full_merge_result) = S ((S (gcomp_merge_index_gfull_full_merge_result)) * c)) /\ exists ff_q_gcrt_gfull_full_merge_result_modulus. b = ff_q_gcrt_gfull_full_merge_result_modulus * S ((S (gcomp_merge_index_gfull_full_merge_result)) * c) + (gcomp_merge_modulus_gfull_full_merge_result))) -> ((((exists hag_left_factor_gcomp_gfull_full_merge_result_gcd. gcomp_merge_lcm_gfull_full_merge_result = gcomp_merge_gcd_gfull_full_merge_result * hag_left_factor_gcomp_gfull_full_merge_result_gcd) /\ (exists hag_right_factor_gcomp_gfull_full_merge_result_gcd. gcomp_merge_modulus_gfull_full_merge_result = gcomp_merge_gcd_gfull_full_merge_result * hag_right_factor_gcomp_gfull_full_merge_result_gcd)) /\ forall hag_divisor_gcomp_gfull_full_merge_result_gcd. (exists hag_common_left_gcomp_gfull_full_merge_result_gcd. gcomp_merge_lcm_gfull_full_merge_result = hag_divisor_gcomp_gfull_full_merge_result_gcd * hag_common_left_gcomp_gfull_full_merge_result_gcd) -> (exists hag_common_right_gcomp_gfull_full_merge_result_gcd. gcomp_merge_modulus_gfull_full_merge_result = hag_divisor_gcomp_gfull_full_merge_result_gcd * hag_common_right_gcomp_gfull_full_merge_result_gcd) -> exists hag_greatest_factor_gcomp_gfull_full_merge_result_gcd. gcomp_merge_gcd_gfull_full_merge_result = hag_divisor_gcomp_gfull_full_merge_result_gcd * hag_greatest_factor_gcomp_gfull_full_merge_result_gcd)) -> (exists hgcrt_mod_left_gcrt_gfull_full_merge_result_result hgcrt_mod_right_gcrt_gfull_full_merge_result_result. gcomp_merge_solution_gfull_full_merge_result + gcomp_merge_gcd_gfull_full_merge_result * hgcrt_mod_left_gcrt_gfull_full_merge_result_result = gcomp_merge_residue_gfull_full_merge_result + gcomp_merge_gcd_gfull_full_merge_result * hgcrt_mod_right_gcrt_gfull_full_merge_result_result))

Complete tactic proof in conservative notation

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

44 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 (2)

crt prefix gcd congruences lcm crt pairwise compatible prefix induces gcd congruences

01Fix variables and assumptionsL1–10

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