FC000F

crt_pairwise_compatible_prefix_canonical_exists_unique

Full constructive canonical generalized CRT for arbitrary finite pairwise-compatible positive moduli: an exact list LCM and a unique strictly bounded simultaneous solution, with no supplied merge invariant or dominating modulus.

Alpha v34 checked-use · first admitted v27 · 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.

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. CRTPositiveModuliPrefix(b,c,l) → CRTPairwiseCompatiblePrefix(r,s,b,c,l) → ∃ x. ∃ y. CRTPrefixLCM(b,c,l,y) ∧ (Lt(x,y) ∧ CRTPrefixSolution(r,s,b,c,l,x)) ∧ (∀ z. CRTPrefixLCM(b,c,l,y) ∧ (Lt(z,y) ∧ CRTPrefixSolution(r,s,b,c,l,z)) → z = x)

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

Definition DAG

CRTPositiveModuliPrefix(b,c,l) · 1CRTPrefixSolution(r,s,b,c,l,x) · 2CRTPrefixLCM(b,c,l,M) · 2CRTPairwiseCompatiblePrefix(r,s,b,c,l) · 1Lt(a,b) · 2

Actual proof prerequisites

crt_pairwise_compatible_prefix_implies_merge_compatiblecrt_merge_compatible_prefix_canonical_exists_unique · checked external prerequisite
Original expanded first-order statement 
forall r s b c l. (forall gcrt_positive_index_gfull_full_canonical_positive gcrt_positive_value_gfull_full_canonical_positive. (exists ff_lt_gcrt_gfull_full_canonical_positive_bound. ff_lt_gcrt_gfull_full_canonical_positive_bound + S gcrt_positive_index_gfull_full_canonical_positive = l) -> (((exists ff_h_gcrt_gfull_full_canonical_positive_entry. ff_h_gcrt_gfull_full_canonical_positive_entry + S (gcrt_positive_value_gfull_full_canonical_positive) = S ((S (gcrt_positive_index_gfull_full_canonical_positive)) * c)) /\ exists ff_q_gcrt_gfull_full_canonical_positive_entry. b = ff_q_gcrt_gfull_full_canonical_positive_entry * S ((S (gcrt_positive_index_gfull_full_canonical_positive)) * c) + (gcrt_positive_value_gfull_full_canonical_positive))) -> ~(gcrt_positive_value_gfull_full_canonical_positive = 0)) -> (forall gcomp_left_index_gfull_full_canonical_pairs gcomp_right_index_gfull_full_canonical_pairs gcomp_left_residue_gfull_full_canonical_pairs gcomp_right_residue_gfull_full_canonical_pairs gcomp_left_modulus_gfull_full_canonical_pairs gcomp_right_modulus_gfull_full_canonical_pairs gcomp_pair_gcd_gfull_full_canonical_pairs. (exists ff_lt_gcrt_gfull_full_canonical_pairs_left_bound. ff_lt_gcrt_gfull_full_canonical_pairs_left_bound + S gcomp_left_index_gfull_full_canonical_pairs = l) -> (exists ff_lt_gcrt_gfull_full_canonical_pairs_right_bound. ff_lt_gcrt_gfull_full_canonical_pairs_right_bound + S gcomp_right_index_gfull_full_canonical_pairs = l) -> (((exists ff_h_gcrt_gfull_full_canonical_pairs_left_residue. ff_h_gcrt_gfull_full_canonical_pairs_left_residue + S (gcomp_left_residue_gfull_full_canonical_pairs) = S ((S (gcomp_left_index_gfull_full_canonical_pairs)) * s)) /\ exists ff_q_gcrt_gfull_full_canonical_pairs_left_residue. r = ff_q_gcrt_gfull_full_canonical_pairs_left_residue * S ((S (gcomp_left_index_gfull_full_canonical_pairs)) * s) + (gcomp_left_residue_gfull_full_canonical_pairs))) -> (((exists ff_h_gcrt_gfull_full_canonical_pairs_right_residue. ff_h_gcrt_gfull_full_canonical_pairs_right_residue + S (gcomp_right_residue_gfull_full_canonical_pairs) = S ((S (gcomp_right_index_gfull_full_canonical_pairs)) * s)) /\ exists ff_q_gcrt_gfull_full_canonical_pairs_right_residue. r = ff_q_gcrt_gfull_full_canonical_pairs_right_residue * S ((S (gcomp_right_index_gfull_full_canonical_pairs)) * s) + (gcomp_right_residue_gfull_full_canonical_pairs))) -> (((exists ff_h_gcrt_gfull_full_canonical_pairs_left_modulus. ff_h_gcrt_gfull_full_canonical_pairs_left_modulus + S (gcomp_left_modulus_gfull_full_canonical_pairs) = S ((S (gcomp_left_index_gfull_full_canonical_pairs)) * c)) /\ exists ff_q_gcrt_gfull_full_canonical_pairs_left_modulus. b = ff_q_gcrt_gfull_full_canonical_pairs_left_modulus * S ((S (gcomp_left_index_gfull_full_canonical_pairs)) * c) + (gcomp_left_modulus_gfull_full_canonical_pairs))) -> (((exists ff_h_gcrt_gfull_full_canonical_pairs_right_modulus. ff_h_gcrt_gfull_full_canonical_pairs_right_modulus + S (gcomp_right_modulus_gfull_full_canonical_pairs) = S ((S (gcomp_right_index_gfull_full_canonical_pairs)) * c)) /\ exists ff_q_gcrt_gfull_full_canonical_pairs_right_modulus. b = ff_q_gcrt_gfull_full_canonical_pairs_right_modulus * S ((S (gcomp_right_index_gfull_full_canonical_pairs)) * c) + (gcomp_right_modulus_gfull_full_canonical_pairs))) -> ((((exists hag_left_factor_gcomp_gfull_full_canonical_pairs_gcd. gcomp_left_modulus_gfull_full_canonical_pairs = gcomp_pair_gcd_gfull_full_canonical_pairs * hag_left_factor_gcomp_gfull_full_canonical_pairs_gcd) /\ (exists hag_right_factor_gcomp_gfull_full_canonical_pairs_gcd. gcomp_right_modulus_gfull_full_canonical_pairs = gcomp_pair_gcd_gfull_full_canonical_pairs * hag_right_factor_gcomp_gfull_full_canonical_pairs_gcd)) /\ forall hag_divisor_gcomp_gfull_full_canonical_pairs_gcd. (exists hag_common_left_gcomp_gfull_full_canonical_pairs_gcd. gcomp_left_modulus_gfull_full_canonical_pairs = hag_divisor_gcomp_gfull_full_canonical_pairs_gcd * hag_common_left_gcomp_gfull_full_canonical_pairs_gcd) -> (exists hag_common_right_gcomp_gfull_full_canonical_pairs_gcd. gcomp_right_modulus_gfull_full_canonical_pairs = hag_divisor_gcomp_gfull_full_canonical_pairs_gcd * hag_common_right_gcomp_gfull_full_canonical_pairs_gcd) -> exists hag_greatest_factor_gcomp_gfull_full_canonical_pairs_gcd. gcomp_pair_gcd_gfull_full_canonical_pairs = hag_divisor_gcomp_gfull_full_canonical_pairs_gcd * hag_greatest_factor_gcomp_gfull_full_canonical_pairs_gcd)) -> (exists hgcrt_mod_left_gcrt_gfull_full_canonical_pairs_result hgcrt_mod_right_gcrt_gfull_full_canonical_pairs_result. gcomp_left_residue_gfull_full_canonical_pairs + gcomp_pair_gcd_gfull_full_canonical_pairs * hgcrt_mod_left_gcrt_gfull_full_canonical_pairs_result = gcomp_right_residue_gfull_full_canonical_pairs + gcomp_pair_gcd_gfull_full_canonical_pairs * hgcrt_mod_right_gcrt_gfull_full_canonical_pairs_result)) -> exists x M. ((((((forall gcrt_common_index_gfull_full_canonical_chosen_lcm_own gcrt_common_modulus_gfull_full_canonical_chosen_lcm_own. (exists ff_lt_gcrt_gfull_full_canonical_chosen_lcm_own_bound. ff_lt_gcrt_gfull_full_canonical_chosen_lcm_own_bound + S gcrt_common_index_gfull_full_canonical_chosen_lcm_own = l) -> (((exists ff_h_gcrt_gfull_full_canonical_chosen_lcm_own_entry. ff_h_gcrt_gfull_full_canonical_chosen_lcm_own_entry + S (gcrt_common_modulus_gfull_full_canonical_chosen_lcm_own) = S ((S (gcrt_common_index_gfull_full_canonical_chosen_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_full_canonical_chosen_lcm_own_entry. b = ff_q_gcrt_gfull_full_canonical_chosen_lcm_own_entry * S ((S (gcrt_common_index_gfull_full_canonical_chosen_lcm_own)) * c) + (gcrt_common_modulus_gfull_full_canonical_chosen_lcm_own))) -> exists gcrt_common_quotient_gfull_full_canonical_chosen_lcm_own. M = gcrt_common_modulus_gfull_full_canonical_chosen_lcm_own * gcrt_common_quotient_gfull_full_canonical_chosen_lcm_own) /\ forall gcrt_lcm_common_gfull_full_canonical_chosen_lcm. (forall gcrt_common_index_gfull_full_canonical_chosen_lcm_other gcrt_common_modulus_gfull_full_canonical_chosen_lcm_other. (exists ff_lt_gcrt_gfull_full_canonical_chosen_lcm_other_bound. ff_lt_gcrt_gfull_full_canonical_chosen_lcm_other_bound + S gcrt_common_index_gfull_full_canonical_chosen_lcm_other = l) -> (((exists ff_h_gcrt_gfull_full_canonical_chosen_lcm_other_entry. ff_h_gcrt_gfull_full_canonical_chosen_lcm_other_entry + S (gcrt_common_modulus_gfull_full_canonical_chosen_lcm_other) = S ((S (gcrt_common_index_gfull_full_canonical_chosen_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_full_canonical_chosen_lcm_other_entry. b = ff_q_gcrt_gfull_full_canonical_chosen_lcm_other_entry * S ((S (gcrt_common_index_gfull_full_canonical_chosen_lcm_other)) * c) + (gcrt_common_modulus_gfull_full_canonical_chosen_lcm_other))) -> exists gcrt_common_quotient_gfull_full_canonical_chosen_lcm_other. gcrt_lcm_common_gfull_full_canonical_chosen_lcm = gcrt_common_modulus_gfull_full_canonical_chosen_lcm_other * gcrt_common_quotient_gfull_full_canonical_chosen_lcm_other) -> exists gcrt_lcm_quotient_gfull_full_canonical_chosen_lcm. gcrt_lcm_common_gfull_full_canonical_chosen_lcm = M * gcrt_lcm_quotient_gfull_full_canonical_chosen_lcm)) /\ ((exists ff_lt_gcrt_gfull_full_canonical_chosen_bounded. ff_lt_gcrt_gfull_full_canonical_chosen_bounded + S x = M) /\ (forall gcrt_solution_index_gfull_full_canonical_chosen_solution gcrt_solution_residue_gfull_full_canonical_chosen_solution gcrt_solution_modulus_gfull_full_canonical_chosen_solution. (exists ff_lt_gcrt_gfull_full_canonical_chosen_solution_bound. ff_lt_gcrt_gfull_full_canonical_chosen_solution_bound + S gcrt_solution_index_gfull_full_canonical_chosen_solution = l) -> (((exists ff_h_gcrt_gfull_full_canonical_chosen_solution_residue. ff_h_gcrt_gfull_full_canonical_chosen_solution_residue + S (gcrt_solution_residue_gfull_full_canonical_chosen_solution) = S ((S (gcrt_solution_index_gfull_full_canonical_chosen_solution)) * s)) /\ exists ff_q_gcrt_gfull_full_canonical_chosen_solution_residue. r = ff_q_gcrt_gfull_full_canonical_chosen_solution_residue * S ((S (gcrt_solution_index_gfull_full_canonical_chosen_solution)) * s) + (gcrt_solution_residue_gfull_full_canonical_chosen_solution))) -> (((exists ff_h_gcrt_gfull_full_canonical_chosen_solution_modulus. ff_h_gcrt_gfull_full_canonical_chosen_solution_modulus + S (gcrt_solution_modulus_gfull_full_canonical_chosen_solution) = S ((S (gcrt_solution_index_gfull_full_canonical_chosen_solution)) * c)) /\ exists ff_q_gcrt_gfull_full_canonical_chosen_solution_modulus. b = ff_q_gcrt_gfull_full_canonical_chosen_solution_modulus * S ((S (gcrt_solution_index_gfull_full_canonical_chosen_solution)) * c) + (gcrt_solution_modulus_gfull_full_canonical_chosen_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_full_canonical_chosen_solution_congruence hgcrt_mod_right_gcrt_gfull_full_canonical_chosen_solution_congruence. x + gcrt_solution_modulus_gfull_full_canonical_chosen_solution * hgcrt_mod_left_gcrt_gfull_full_canonical_chosen_solution_congruence = gcrt_solution_residue_gfull_full_canonical_chosen_solution + gcrt_solution_modulus_gfull_full_canonical_chosen_solution * hgcrt_mod_right_gcrt_gfull_full_canonical_chosen_solution_congruence))))) /\ forall y. (((((forall gcrt_common_index_gfull_full_canonical_compared_lcm_own gcrt_common_modulus_gfull_full_canonical_compared_lcm_own. (exists ff_lt_gcrt_gfull_full_canonical_compared_lcm_own_bound. ff_lt_gcrt_gfull_full_canonical_compared_lcm_own_bound + S gcrt_common_index_gfull_full_canonical_compared_lcm_own = l) -> (((exists ff_h_gcrt_gfull_full_canonical_compared_lcm_own_entry. ff_h_gcrt_gfull_full_canonical_compared_lcm_own_entry + S (gcrt_common_modulus_gfull_full_canonical_compared_lcm_own) = S ((S (gcrt_common_index_gfull_full_canonical_compared_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_full_canonical_compared_lcm_own_entry. b = ff_q_gcrt_gfull_full_canonical_compared_lcm_own_entry * S ((S (gcrt_common_index_gfull_full_canonical_compared_lcm_own)) * c) + (gcrt_common_modulus_gfull_full_canonical_compared_lcm_own))) -> exists gcrt_common_quotient_gfull_full_canonical_compared_lcm_own. M = gcrt_common_modulus_gfull_full_canonical_compared_lcm_own * gcrt_common_quotient_gfull_full_canonical_compared_lcm_own) /\ forall gcrt_lcm_common_gfull_full_canonical_compared_lcm. (forall gcrt_common_index_gfull_full_canonical_compared_lcm_other gcrt_common_modulus_gfull_full_canonical_compared_lcm_other. (exists ff_lt_gcrt_gfull_full_canonical_compared_lcm_other_bound. ff_lt_gcrt_gfull_full_canonical_compared_lcm_other_bound + S gcrt_common_index_gfull_full_canonical_compared_lcm_other = l) -> (((exists ff_h_gcrt_gfull_full_canonical_compared_lcm_other_entry. ff_h_gcrt_gfull_full_canonical_compared_lcm_other_entry + S (gcrt_common_modulus_gfull_full_canonical_compared_lcm_other) = S ((S (gcrt_common_index_gfull_full_canonical_compared_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_full_canonical_compared_lcm_other_entry. b = ff_q_gcrt_gfull_full_canonical_compared_lcm_other_entry * S ((S (gcrt_common_index_gfull_full_canonical_compared_lcm_other)) * c) + (gcrt_common_modulus_gfull_full_canonical_compared_lcm_other))) -> exists gcrt_common_quotient_gfull_full_canonical_compared_lcm_other. gcrt_lcm_common_gfull_full_canonical_compared_lcm = gcrt_common_modulus_gfull_full_canonical_compared_lcm_other * gcrt_common_quotient_gfull_full_canonical_compared_lcm_other) -> exists gcrt_lcm_quotient_gfull_full_canonical_compared_lcm. gcrt_lcm_common_gfull_full_canonical_compared_lcm = M * gcrt_lcm_quotient_gfull_full_canonical_compared_lcm)) /\ ((exists ff_lt_gcrt_gfull_full_canonical_compared_bounded. ff_lt_gcrt_gfull_full_canonical_compared_bounded + S y = M) /\ (forall gcrt_solution_index_gfull_full_canonical_compared_solution gcrt_solution_residue_gfull_full_canonical_compared_solution gcrt_solution_modulus_gfull_full_canonical_compared_solution. (exists ff_lt_gcrt_gfull_full_canonical_compared_solution_bound. ff_lt_gcrt_gfull_full_canonical_compared_solution_bound + S gcrt_solution_index_gfull_full_canonical_compared_solution = l) -> (((exists ff_h_gcrt_gfull_full_canonical_compared_solution_residue. ff_h_gcrt_gfull_full_canonical_compared_solution_residue + S (gcrt_solution_residue_gfull_full_canonical_compared_solution) = S ((S (gcrt_solution_index_gfull_full_canonical_compared_solution)) * s)) /\ exists ff_q_gcrt_gfull_full_canonical_compared_solution_residue. r = ff_q_gcrt_gfull_full_canonical_compared_solution_residue * S ((S (gcrt_solution_index_gfull_full_canonical_compared_solution)) * s) + (gcrt_solution_residue_gfull_full_canonical_compared_solution))) -> (((exists ff_h_gcrt_gfull_full_canonical_compared_solution_modulus. ff_h_gcrt_gfull_full_canonical_compared_solution_modulus + S (gcrt_solution_modulus_gfull_full_canonical_compared_solution) = S ((S (gcrt_solution_index_gfull_full_canonical_compared_solution)) * c)) /\ exists ff_q_gcrt_gfull_full_canonical_compared_solution_modulus. b = ff_q_gcrt_gfull_full_canonical_compared_solution_modulus * S ((S (gcrt_solution_index_gfull_full_canonical_compared_solution)) * c) + (gcrt_solution_modulus_gfull_full_canonical_compared_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_full_canonical_compared_solution_congruence hgcrt_mod_right_gcrt_gfull_full_canonical_compared_solution_congruence. y + gcrt_solution_modulus_gfull_full_canonical_compared_solution * hgcrt_mod_left_gcrt_gfull_full_canonical_compared_solution_congruence = gcrt_solution_residue_gfull_full_canonical_compared_solution + gcrt_solution_modulus_gfull_full_canonical_compared_solution * hgcrt_mod_right_gcrt_gfull_full_canonical_compared_solution_congruence))))) -> y = x)

Complete tactic proof in conservative notation

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

21 script commands · 3 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 pairwise compatible prefix implies merge compatible
01Fix variables and assumptionsL1–7

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 hpositive
  7. L7
    intro hp
02Use earlier factsL8–17

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

  1. L8
    specialize crt_merge_compatible_prefix_canonical_exists_unique r
  2. L9
    specialize crt_merge_compatible_prefix_canonical_exists_unique s
  3. L10
    specialize crt_merge_compatible_prefix_canonical_exists_unique b
  4. L11
    specialize crt_merge_compatible_prefix_canonical_exists_unique c
  5. L12
    specialize crt_merge_compatible_prefix_canonical_exists_unique l
  6. L13
    apply crt_merge_compatible_prefix_canonical_exists_unique
  7. L14
    exact hpositive
  8. L15
    specialize crt_pairwise_compatible_prefix_implies_merge_compatible r
  9. L16
    specialize crt_pairwise_compatible_prefix_implies_merge_compatible s
  10. L17
    specialize crt_pairwise_compatible_prefix_implies_merge_compatible b
03Use earlier factsL18–21

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

  1. L18
    specialize crt_pairwise_compatible_prefix_implies_merge_compatible c
  2. L19
    specialize crt_pairwise_compatible_prefix_implies_merge_compatible l
  3. L20
    apply crt_pairwise_compatible_prefix_implies_merge_compatible
  4. L21
    exact hp

Library-wide reading audit

Original defined command ledger · 21 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro hpositive
  7. 0007intro hp
  8. 0008specialize crt_merge_compatible_prefix_canonical_exists_unique r
  9. 0009specialize crt_merge_compatible_prefix_canonical_exists_unique s
  10. 0010specialize crt_merge_compatible_prefix_canonical_exists_unique b
  11. 0011specialize crt_merge_compatible_prefix_canonical_exists_unique c
  12. 0012specialize crt_merge_compatible_prefix_canonical_exists_unique l
  13. 0013apply crt_merge_compatible_prefix_canonical_exists_unique
  14. 0014exact hpositive
  15. 0015specialize crt_pairwise_compatible_prefix_implies_merge_compatible r
  16. 0016specialize crt_pairwise_compatible_prefix_implies_merge_compatible s
  17. 0017specialize crt_pairwise_compatible_prefix_implies_merge_compatible b
  18. 0018specialize crt_pairwise_compatible_prefix_implies_merge_compatible c
  19. 0019specialize crt_pairwise_compatible_prefix_implies_merge_compatible l
  20. 0020apply crt_pairwise_compatible_prefix_implies_merge_compatible
  21. 0021exact hp