GC0016

crt_merge_compatible_prefix_implies_pairwise_compatible

The operational predecessor-LCM merge invariant constructively implies exact pairwise gcd compatibility; the converse is not assumed.

Alpha v34 checked-use · first admitted v25 · 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 under successive-merge compatibility and in the pairwise-compatible dominating-last case. G011 is now closed in the separate Alpha-v27 generalized-crt branch for arbitrary pairwise-compatible finite lists, including noncoprime moduli. Full G011 proof · Alpha v27

Exact theorem in conservative defined notation

∀ r. ∀ s. ∀ b. ∀ c. ∀ l. CRTMergeCompatiblePrefix(r,s,b,c,l) → CRTPairwiseCompatiblePrefix(r,s,b,c,l)

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

Definition DAG

CRTPairwiseCompatiblePrefix(r,s,b,c,l) · 1CRTMergeCompatiblePrefix(r,s,b,c,l) · 1

Actual proof prerequisites

crt_merge_compatible_prefix_solution_existscrt_prefix_solution_implies_pairwise_compatible
Original expanded first-order statement 
forall r s b c l. (forall gcomp_merge_index_merge_implies_pairwise_source gcomp_merge_solution_merge_implies_pairwise_source gcomp_merge_lcm_merge_implies_pairwise_source gcomp_merge_residue_merge_implies_pairwise_source gcomp_merge_modulus_merge_implies_pairwise_source gcomp_merge_gcd_merge_implies_pairwise_source. (exists ff_lt_gcrt_merge_implies_pairwise_source_bound. ff_lt_gcrt_merge_implies_pairwise_source_bound + S gcomp_merge_index_merge_implies_pairwise_source = l) -> (((forall gcrt_common_index_merge_implies_pairwise_source_lcm_own gcrt_common_modulus_merge_implies_pairwise_source_lcm_own. (exists ff_lt_gcrt_merge_implies_pairwise_source_lcm_own_bound. ff_lt_gcrt_merge_implies_pairwise_source_lcm_own_bound + S gcrt_common_index_merge_implies_pairwise_source_lcm_own = gcomp_merge_index_merge_implies_pairwise_source) -> (((exists ff_h_gcrt_merge_implies_pairwise_source_lcm_own_entry. ff_h_gcrt_merge_implies_pairwise_source_lcm_own_entry + S (gcrt_common_modulus_merge_implies_pairwise_source_lcm_own) = S ((S (gcrt_common_index_merge_implies_pairwise_source_lcm_own)) * c)) /\ exists ff_q_gcrt_merge_implies_pairwise_source_lcm_own_entry. b = ff_q_gcrt_merge_implies_pairwise_source_lcm_own_entry * S ((S (gcrt_common_index_merge_implies_pairwise_source_lcm_own)) * c) + (gcrt_common_modulus_merge_implies_pairwise_source_lcm_own))) -> exists gcrt_common_quotient_merge_implies_pairwise_source_lcm_own. gcomp_merge_lcm_merge_implies_pairwise_source = gcrt_common_modulus_merge_implies_pairwise_source_lcm_own * gcrt_common_quotient_merge_implies_pairwise_source_lcm_own) /\ forall gcrt_lcm_common_merge_implies_pairwise_source_lcm. (forall gcrt_common_index_merge_implies_pairwise_source_lcm_other gcrt_common_modulus_merge_implies_pairwise_source_lcm_other. (exists ff_lt_gcrt_merge_implies_pairwise_source_lcm_other_bound. ff_lt_gcrt_merge_implies_pairwise_source_lcm_other_bound + S gcrt_common_index_merge_implies_pairwise_source_lcm_other = gcomp_merge_index_merge_implies_pairwise_source) -> (((exists ff_h_gcrt_merge_implies_pairwise_source_lcm_other_entry. ff_h_gcrt_merge_implies_pairwise_source_lcm_other_entry + S (gcrt_common_modulus_merge_implies_pairwise_source_lcm_other) = S ((S (gcrt_common_index_merge_implies_pairwise_source_lcm_other)) * c)) /\ exists ff_q_gcrt_merge_implies_pairwise_source_lcm_other_entry. b = ff_q_gcrt_merge_implies_pairwise_source_lcm_other_entry * S ((S (gcrt_common_index_merge_implies_pairwise_source_lcm_other)) * c) + (gcrt_common_modulus_merge_implies_pairwise_source_lcm_other))) -> exists gcrt_common_quotient_merge_implies_pairwise_source_lcm_other. gcrt_lcm_common_merge_implies_pairwise_source_lcm = gcrt_common_modulus_merge_implies_pairwise_source_lcm_other * gcrt_common_quotient_merge_implies_pairwise_source_lcm_other) -> exists gcrt_lcm_quotient_merge_implies_pairwise_source_lcm. gcrt_lcm_common_merge_implies_pairwise_source_lcm = gcomp_merge_lcm_merge_implies_pairwise_source * gcrt_lcm_quotient_merge_implies_pairwise_source_lcm)) -> (forall gcrt_solution_index_merge_implies_pairwise_source_solution gcrt_solution_residue_merge_implies_pairwise_source_solution gcrt_solution_modulus_merge_implies_pairwise_source_solution. (exists ff_lt_gcrt_merge_implies_pairwise_source_solution_bound. ff_lt_gcrt_merge_implies_pairwise_source_solution_bound + S gcrt_solution_index_merge_implies_pairwise_source_solution = gcomp_merge_index_merge_implies_pairwise_source) -> (((exists ff_h_gcrt_merge_implies_pairwise_source_solution_residue. ff_h_gcrt_merge_implies_pairwise_source_solution_residue + S (gcrt_solution_residue_merge_implies_pairwise_source_solution) = S ((S (gcrt_solution_index_merge_implies_pairwise_source_solution)) * s)) /\ exists ff_q_gcrt_merge_implies_pairwise_source_solution_residue. r = ff_q_gcrt_merge_implies_pairwise_source_solution_residue * S ((S (gcrt_solution_index_merge_implies_pairwise_source_solution)) * s) + (gcrt_solution_residue_merge_implies_pairwise_source_solution))) -> (((exists ff_h_gcrt_merge_implies_pairwise_source_solution_modulus. ff_h_gcrt_merge_implies_pairwise_source_solution_modulus + S (gcrt_solution_modulus_merge_implies_pairwise_source_solution) = S ((S (gcrt_solution_index_merge_implies_pairwise_source_solution)) * c)) /\ exists ff_q_gcrt_merge_implies_pairwise_source_solution_modulus. b = ff_q_gcrt_merge_implies_pairwise_source_solution_modulus * S ((S (gcrt_solution_index_merge_implies_pairwise_source_solution)) * c) + (gcrt_solution_modulus_merge_implies_pairwise_source_solution))) -> (exists hgcrt_mod_left_gcrt_merge_implies_pairwise_source_solution_congruence hgcrt_mod_right_gcrt_merge_implies_pairwise_source_solution_congruence. gcomp_merge_solution_merge_implies_pairwise_source + gcrt_solution_modulus_merge_implies_pairwise_source_solution * hgcrt_mod_left_gcrt_merge_implies_pairwise_source_solution_congruence = gcrt_solution_residue_merge_implies_pairwise_source_solution + gcrt_solution_modulus_merge_implies_pairwise_source_solution * hgcrt_mod_right_gcrt_merge_implies_pairwise_source_solution_congruence)) -> (((exists ff_h_gcrt_merge_implies_pairwise_source_residue. ff_h_gcrt_merge_implies_pairwise_source_residue + S (gcomp_merge_residue_merge_implies_pairwise_source) = S ((S (gcomp_merge_index_merge_implies_pairwise_source)) * s)) /\ exists ff_q_gcrt_merge_implies_pairwise_source_residue. r = ff_q_gcrt_merge_implies_pairwise_source_residue * S ((S (gcomp_merge_index_merge_implies_pairwise_source)) * s) + (gcomp_merge_residue_merge_implies_pairwise_source))) -> (((exists ff_h_gcrt_merge_implies_pairwise_source_modulus. ff_h_gcrt_merge_implies_pairwise_source_modulus + S (gcomp_merge_modulus_merge_implies_pairwise_source) = S ((S (gcomp_merge_index_merge_implies_pairwise_source)) * c)) /\ exists ff_q_gcrt_merge_implies_pairwise_source_modulus. b = ff_q_gcrt_merge_implies_pairwise_source_modulus * S ((S (gcomp_merge_index_merge_implies_pairwise_source)) * c) + (gcomp_merge_modulus_merge_implies_pairwise_source))) -> ((((exists hag_left_factor_gcomp_merge_implies_pairwise_source_gcd. gcomp_merge_lcm_merge_implies_pairwise_source = gcomp_merge_gcd_merge_implies_pairwise_source * hag_left_factor_gcomp_merge_implies_pairwise_source_gcd) /\ (exists hag_right_factor_gcomp_merge_implies_pairwise_source_gcd. gcomp_merge_modulus_merge_implies_pairwise_source = gcomp_merge_gcd_merge_implies_pairwise_source * hag_right_factor_gcomp_merge_implies_pairwise_source_gcd)) /\ forall hag_divisor_gcomp_merge_implies_pairwise_source_gcd. (exists hag_common_left_gcomp_merge_implies_pairwise_source_gcd. gcomp_merge_lcm_merge_implies_pairwise_source = hag_divisor_gcomp_merge_implies_pairwise_source_gcd * hag_common_left_gcomp_merge_implies_pairwise_source_gcd) -> (exists hag_common_right_gcomp_merge_implies_pairwise_source_gcd. gcomp_merge_modulus_merge_implies_pairwise_source = hag_divisor_gcomp_merge_implies_pairwise_source_gcd * hag_common_right_gcomp_merge_implies_pairwise_source_gcd) -> exists hag_greatest_factor_gcomp_merge_implies_pairwise_source_gcd. gcomp_merge_gcd_merge_implies_pairwise_source = hag_divisor_gcomp_merge_implies_pairwise_source_gcd * hag_greatest_factor_gcomp_merge_implies_pairwise_source_gcd)) -> (exists hgcrt_mod_left_gcrt_merge_implies_pairwise_source_result hgcrt_mod_right_gcrt_merge_implies_pairwise_source_result. gcomp_merge_solution_merge_implies_pairwise_source + gcomp_merge_gcd_merge_implies_pairwise_source * hgcrt_mod_left_gcrt_merge_implies_pairwise_source_result = gcomp_merge_residue_merge_implies_pairwise_source + gcomp_merge_gcd_merge_implies_pairwise_source * hgcrt_mod_right_gcrt_merge_implies_pairwise_source_result)) -> (forall gcomp_left_index_merge_implies_pairwise_result gcomp_right_index_merge_implies_pairwise_result gcomp_left_residue_merge_implies_pairwise_result gcomp_right_residue_merge_implies_pairwise_result gcomp_left_modulus_merge_implies_pairwise_result gcomp_right_modulus_merge_implies_pairwise_result gcomp_pair_gcd_merge_implies_pairwise_result. (exists ff_lt_gcrt_merge_implies_pairwise_result_left_bound. ff_lt_gcrt_merge_implies_pairwise_result_left_bound + S gcomp_left_index_merge_implies_pairwise_result = l) -> (exists ff_lt_gcrt_merge_implies_pairwise_result_right_bound. ff_lt_gcrt_merge_implies_pairwise_result_right_bound + S gcomp_right_index_merge_implies_pairwise_result = l) -> (((exists ff_h_gcrt_merge_implies_pairwise_result_left_residue. ff_h_gcrt_merge_implies_pairwise_result_left_residue + S (gcomp_left_residue_merge_implies_pairwise_result) = S ((S (gcomp_left_index_merge_implies_pairwise_result)) * s)) /\ exists ff_q_gcrt_merge_implies_pairwise_result_left_residue. r = ff_q_gcrt_merge_implies_pairwise_result_left_residue * S ((S (gcomp_left_index_merge_implies_pairwise_result)) * s) + (gcomp_left_residue_merge_implies_pairwise_result))) -> (((exists ff_h_gcrt_merge_implies_pairwise_result_right_residue. ff_h_gcrt_merge_implies_pairwise_result_right_residue + S (gcomp_right_residue_merge_implies_pairwise_result) = S ((S (gcomp_right_index_merge_implies_pairwise_result)) * s)) /\ exists ff_q_gcrt_merge_implies_pairwise_result_right_residue. r = ff_q_gcrt_merge_implies_pairwise_result_right_residue * S ((S (gcomp_right_index_merge_implies_pairwise_result)) * s) + (gcomp_right_residue_merge_implies_pairwise_result))) -> (((exists ff_h_gcrt_merge_implies_pairwise_result_left_modulus. ff_h_gcrt_merge_implies_pairwise_result_left_modulus + S (gcomp_left_modulus_merge_implies_pairwise_result) = S ((S (gcomp_left_index_merge_implies_pairwise_result)) * c)) /\ exists ff_q_gcrt_merge_implies_pairwise_result_left_modulus. b = ff_q_gcrt_merge_implies_pairwise_result_left_modulus * S ((S (gcomp_left_index_merge_implies_pairwise_result)) * c) + (gcomp_left_modulus_merge_implies_pairwise_result))) -> (((exists ff_h_gcrt_merge_implies_pairwise_result_right_modulus. ff_h_gcrt_merge_implies_pairwise_result_right_modulus + S (gcomp_right_modulus_merge_implies_pairwise_result) = S ((S (gcomp_right_index_merge_implies_pairwise_result)) * c)) /\ exists ff_q_gcrt_merge_implies_pairwise_result_right_modulus. b = ff_q_gcrt_merge_implies_pairwise_result_right_modulus * S ((S (gcomp_right_index_merge_implies_pairwise_result)) * c) + (gcomp_right_modulus_merge_implies_pairwise_result))) -> ((((exists hag_left_factor_gcomp_merge_implies_pairwise_result_gcd. gcomp_left_modulus_merge_implies_pairwise_result = gcomp_pair_gcd_merge_implies_pairwise_result * hag_left_factor_gcomp_merge_implies_pairwise_result_gcd) /\ (exists hag_right_factor_gcomp_merge_implies_pairwise_result_gcd. gcomp_right_modulus_merge_implies_pairwise_result = gcomp_pair_gcd_merge_implies_pairwise_result * hag_right_factor_gcomp_merge_implies_pairwise_result_gcd)) /\ forall hag_divisor_gcomp_merge_implies_pairwise_result_gcd. (exists hag_common_left_gcomp_merge_implies_pairwise_result_gcd. gcomp_left_modulus_merge_implies_pairwise_result = hag_divisor_gcomp_merge_implies_pairwise_result_gcd * hag_common_left_gcomp_merge_implies_pairwise_result_gcd) -> (exists hag_common_right_gcomp_merge_implies_pairwise_result_gcd. gcomp_right_modulus_merge_implies_pairwise_result = hag_divisor_gcomp_merge_implies_pairwise_result_gcd * hag_common_right_gcomp_merge_implies_pairwise_result_gcd) -> exists hag_greatest_factor_gcomp_merge_implies_pairwise_result_gcd. gcomp_pair_gcd_merge_implies_pairwise_result = hag_divisor_gcomp_merge_implies_pairwise_result_gcd * hag_greatest_factor_gcomp_merge_implies_pairwise_result_gcd)) -> (exists hgcrt_mod_left_gcrt_merge_implies_pairwise_result_result hgcrt_mod_right_gcrt_merge_implies_pairwise_result_result. gcomp_left_residue_merge_implies_pairwise_result + gcomp_pair_gcd_merge_implies_pairwise_result * hgcrt_mod_left_gcrt_merge_implies_pairwise_result_result = gcomp_right_residue_merge_implies_pairwise_result + gcomp_pair_gcd_merge_implies_pairwise_result * hgcrt_mod_right_gcrt_merge_implies_pairwise_result_result))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

23 script commands · 5 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 (2)
crt merge compatible prefix solution existscrt prefix solution implies pairwise compatible

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–6

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

  1. L1
    intro r
  2. L2
    intro s
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro l
  6. L6
    intro hmerge
02Use earlier factsL7–11

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

  1. L7
    specialize crt_merge_compatible_prefix_solution_exists r
  2. L8
    specialize crt_merge_compatible_prefix_solution_exists s
  3. L9
    specialize crt_merge_compatible_prefix_solution_exists b
  4. L10
    specialize crt_merge_compatible_prefix_solution_exists c
  5. L11
    specialize crt_merge_compatible_prefix_solution_exists l
03Establish hsolutionL12–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt merge compatible prefix solution exists.

  1. L12
    have hsolution : ∃ x. CRTPrefixSolution(r,s,b,c,l,x)Definitions: CRTPrefixSolutionOriginal native command in the exact edition
  2. L13
    apply crt_merge_compatible_prefix_solution_exists
  3. L14
    exact hmerge
04Separate the logical casesL15–15

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

  1. L15
    cases hsolution
05Use earlier factsL16–23

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

  1. L16
    specialize crt_prefix_solution_implies_pairwise_compatible r
  2. L17
    specialize crt_prefix_solution_implies_pairwise_compatible s
  3. L18
    specialize crt_prefix_solution_implies_pairwise_compatible b
  4. L19
    specialize crt_prefix_solution_implies_pairwise_compatible c
  5. L20
    specialize crt_prefix_solution_implies_pairwise_compatible l
  6. L21
    specialize crt_prefix_solution_implies_pairwise_compatible x
  7. L22
    apply crt_prefix_solution_implies_pairwise_compatible
  8. L23
    exact hsolution_witness

Library-wide reading audit

Original defined command ledger · 23 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro hmerge
  7. 0007specialize crt_merge_compatible_prefix_solution_exists r
  8. 0008specialize crt_merge_compatible_prefix_solution_exists s
  9. 0009specialize crt_merge_compatible_prefix_solution_exists b
  10. 0010specialize crt_merge_compatible_prefix_solution_exists c
  11. 0011specialize crt_merge_compatible_prefix_solution_exists l
  12. 0012have hsolution : exists x. (forall gcrt_solution_index_gcomp_implies_actual_solution gcrt_solution_residue_gcomp_implies_actual_solution gcrt_solution_modulus_gcomp_implies_actual_solution. (exists ff_lt_gcrt_gcomp_implies_actual_solution_bound. ff_lt_gcrt_gcomp_implies_actual_solution_bound + S gcrt_solution_index_gcomp_implies_actual_solution = l) -> (((exists ff_h_gcrt_gcomp_implies_actual_solution_residue. ff_h_gcrt_gcomp_implies_actual_solution_residue + S (gcrt_solution_residue_gcomp_implies_actual_solution) = S ((S (gcrt_solution_index_gcomp_implies_actual_solution)) * s)) /\ exists ff_q_gcrt_gcomp_implies_actual_solution_residue. r = ff_q_gcrt_gcomp_implies_actual_solution_residue * S ((S (gcrt_solution_index_gcomp_implies_actual_solution)) * s) + (gcrt_solution_residue_gcomp_implies_actual_solution))) -> (((exists ff_h_gcrt_gcomp_implies_actual_solution_modulus. ff_h_gcrt_gcomp_implies_actual_solution_modulus + S (gcrt_solution_modulus_gcomp_implies_actual_solution) = S ((S (gcrt_solution_index_gcomp_implies_actual_solution)) * c)) /\ exists ff_q_gcrt_gcomp_implies_actual_solution_modulus. b = ff_q_gcrt_gcomp_implies_actual_solution_modulus * S ((S (gcrt_solution_index_gcomp_implies_actual_solution)) * c) + (gcrt_solution_modulus_gcomp_implies_actual_solution))) -> (exists hgcrt_mod_left_gcrt_gcomp_implies_actual_solution_congruence hgcrt_mod_right_gcrt_gcomp_implies_actual_solution_congruence. x + gcrt_solution_modulus_gcomp_implies_actual_solution * hgcrt_mod_left_gcrt_gcomp_implies_actual_solution_congruence = gcrt_solution_residue_gcomp_implies_actual_solution + gcrt_solution_modulus_gcomp_implies_actual_solution * hgcrt_mod_right_gcrt_gcomp_implies_actual_solution_congruence))
  13. 0013apply crt_merge_compatible_prefix_solution_exists
  14. 0014exact hmerge
  15. 0015cases hsolution
  16. 0016specialize crt_prefix_solution_implies_pairwise_compatible r
  17. 0017specialize crt_prefix_solution_implies_pairwise_compatible s
  18. 0018specialize crt_prefix_solution_implies_pairwise_compatible b
  19. 0019specialize crt_prefix_solution_implies_pairwise_compatible c
  20. 0020specialize crt_prefix_solution_implies_pairwise_compatible l
  21. 0021specialize crt_prefix_solution_implies_pairwise_compatible x
  22. 0022apply crt_prefix_solution_implies_pairwise_compatible
  23. 0023exact hsolution_witness