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.

Exact expanded first-order arithmetic 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))

Constructive proof overview

Generated structural guide

Every pairwise gcd-compatible finite list satisfies every actual predecessor-LCM merge condition, including arbitrary noncoprime and zero moduli.

The unchanged tactic script uses 2 declared prerequisites and contains 44 exact native proof lines.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

FC000B crt_prefix_gcd_congruences_lcm FC000C crt_pairwise_compatible_prefix_induces_gcd_congruences

Direct dependents

FC000E crt_pairwise_compatible_prefix_solution_exists FC000F crt_pairwise_compatible_prefix_canonical_exists_unique FC0015 crt_pairwise_compatible_prefix_merge_iff

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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.