GC0017

crt_pairwise_compatible_dominating_last_solution

Whenever the last modulus is an actual common multiple of all predecessors, exact pairwise gcd compatibility makes the last residue itself a simultaneous solution, including zero and non-coprime moduli.

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. ∀ a. ∀ M. CRTPairwiseCompatiblePrefix(r,s,b,c,S l) → Beta(r,s,l,a) → Beta(b,c,l,M) → (∀ x. ∀ y. Lt(x,l) → Beta(b,c,x,y) → Dvd(y,M)) → CRTPrefixSolution(r,s,b,c,S l,a)

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

Definition DAG

Beta(b,c,i,x) · 3CRTPrefixSolution(r,s,b,c,l,x) · 1CRTPairwiseCompatiblePrefix(r,s,b,c,l) · 1Lt(a,b) · 1Dvd(d,n) · 1

Actual proof prerequisites

crt_prefix_solution_successor_intro · checked external prerequisiteis_gcd_of_dvd · checked external prerequisitecrt_pairwise_compatible_prefix_lastmod_eq_symm · checked external prerequisitemod_eq_refl · checked external prerequisite
Original expanded first-order statement 
forall r s b c l a M. (forall gcomp_left_index_dominating_pairs gcomp_right_index_dominating_pairs gcomp_left_residue_dominating_pairs gcomp_right_residue_dominating_pairs gcomp_left_modulus_dominating_pairs gcomp_right_modulus_dominating_pairs gcomp_pair_gcd_dominating_pairs. (exists ff_lt_gcrt_dominating_pairs_left_bound. ff_lt_gcrt_dominating_pairs_left_bound + S gcomp_left_index_dominating_pairs = S l) -> (exists ff_lt_gcrt_dominating_pairs_right_bound. ff_lt_gcrt_dominating_pairs_right_bound + S gcomp_right_index_dominating_pairs = S l) -> (((exists ff_h_gcrt_dominating_pairs_left_residue. ff_h_gcrt_dominating_pairs_left_residue + S (gcomp_left_residue_dominating_pairs) = S ((S (gcomp_left_index_dominating_pairs)) * s)) /\ exists ff_q_gcrt_dominating_pairs_left_residue. r = ff_q_gcrt_dominating_pairs_left_residue * S ((S (gcomp_left_index_dominating_pairs)) * s) + (gcomp_left_residue_dominating_pairs))) -> (((exists ff_h_gcrt_dominating_pairs_right_residue. ff_h_gcrt_dominating_pairs_right_residue + S (gcomp_right_residue_dominating_pairs) = S ((S (gcomp_right_index_dominating_pairs)) * s)) /\ exists ff_q_gcrt_dominating_pairs_right_residue. r = ff_q_gcrt_dominating_pairs_right_residue * S ((S (gcomp_right_index_dominating_pairs)) * s) + (gcomp_right_residue_dominating_pairs))) -> (((exists ff_h_gcrt_dominating_pairs_left_modulus. ff_h_gcrt_dominating_pairs_left_modulus + S (gcomp_left_modulus_dominating_pairs) = S ((S (gcomp_left_index_dominating_pairs)) * c)) /\ exists ff_q_gcrt_dominating_pairs_left_modulus. b = ff_q_gcrt_dominating_pairs_left_modulus * S ((S (gcomp_left_index_dominating_pairs)) * c) + (gcomp_left_modulus_dominating_pairs))) -> (((exists ff_h_gcrt_dominating_pairs_right_modulus. ff_h_gcrt_dominating_pairs_right_modulus + S (gcomp_right_modulus_dominating_pairs) = S ((S (gcomp_right_index_dominating_pairs)) * c)) /\ exists ff_q_gcrt_dominating_pairs_right_modulus. b = ff_q_gcrt_dominating_pairs_right_modulus * S ((S (gcomp_right_index_dominating_pairs)) * c) + (gcomp_right_modulus_dominating_pairs))) -> ((((exists hag_left_factor_gcomp_dominating_pairs_gcd. gcomp_left_modulus_dominating_pairs = gcomp_pair_gcd_dominating_pairs * hag_left_factor_gcomp_dominating_pairs_gcd) /\ (exists hag_right_factor_gcomp_dominating_pairs_gcd. gcomp_right_modulus_dominating_pairs = gcomp_pair_gcd_dominating_pairs * hag_right_factor_gcomp_dominating_pairs_gcd)) /\ forall hag_divisor_gcomp_dominating_pairs_gcd. (exists hag_common_left_gcomp_dominating_pairs_gcd. gcomp_left_modulus_dominating_pairs = hag_divisor_gcomp_dominating_pairs_gcd * hag_common_left_gcomp_dominating_pairs_gcd) -> (exists hag_common_right_gcomp_dominating_pairs_gcd. gcomp_right_modulus_dominating_pairs = hag_divisor_gcomp_dominating_pairs_gcd * hag_common_right_gcomp_dominating_pairs_gcd) -> exists hag_greatest_factor_gcomp_dominating_pairs_gcd. gcomp_pair_gcd_dominating_pairs = hag_divisor_gcomp_dominating_pairs_gcd * hag_greatest_factor_gcomp_dominating_pairs_gcd)) -> (exists hgcrt_mod_left_gcrt_dominating_pairs_result hgcrt_mod_right_gcrt_dominating_pairs_result. gcomp_left_residue_dominating_pairs + gcomp_pair_gcd_dominating_pairs * hgcrt_mod_left_gcrt_dominating_pairs_result = gcomp_right_residue_dominating_pairs + gcomp_pair_gcd_dominating_pairs * hgcrt_mod_right_gcrt_dominating_pairs_result)) -> (((exists ff_h_gcrt_dominating_residue. ff_h_gcrt_dominating_residue + S (a) = S ((S (l)) * s)) /\ exists ff_q_gcrt_dominating_residue. r = ff_q_gcrt_dominating_residue * S ((S (l)) * s) + (a))) -> (((exists ff_h_gcrt_dominating_modulus. ff_h_gcrt_dominating_modulus + S (M) = S ((S (l)) * c)) /\ exists ff_q_gcrt_dominating_modulus. b = ff_q_gcrt_dominating_modulus * S ((S (l)) * c) + (M))) -> (forall gcrt_common_index_dominating_common gcrt_common_modulus_dominating_common. (exists ff_lt_gcrt_dominating_common_bound. ff_lt_gcrt_dominating_common_bound + S gcrt_common_index_dominating_common = l) -> (((exists ff_h_gcrt_dominating_common_entry. ff_h_gcrt_dominating_common_entry + S (gcrt_common_modulus_dominating_common) = S ((S (gcrt_common_index_dominating_common)) * c)) /\ exists ff_q_gcrt_dominating_common_entry. b = ff_q_gcrt_dominating_common_entry * S ((S (gcrt_common_index_dominating_common)) * c) + (gcrt_common_modulus_dominating_common))) -> exists gcrt_common_quotient_dominating_common. M = gcrt_common_modulus_dominating_common * gcrt_common_quotient_dominating_common) -> (forall gcrt_solution_index_dominating_solution gcrt_solution_residue_dominating_solution gcrt_solution_modulus_dominating_solution. (exists ff_lt_gcrt_dominating_solution_bound. ff_lt_gcrt_dominating_solution_bound + S gcrt_solution_index_dominating_solution = S l) -> (((exists ff_h_gcrt_dominating_solution_residue. ff_h_gcrt_dominating_solution_residue + S (gcrt_solution_residue_dominating_solution) = S ((S (gcrt_solution_index_dominating_solution)) * s)) /\ exists ff_q_gcrt_dominating_solution_residue. r = ff_q_gcrt_dominating_solution_residue * S ((S (gcrt_solution_index_dominating_solution)) * s) + (gcrt_solution_residue_dominating_solution))) -> (((exists ff_h_gcrt_dominating_solution_modulus. ff_h_gcrt_dominating_solution_modulus + S (gcrt_solution_modulus_dominating_solution) = S ((S (gcrt_solution_index_dominating_solution)) * c)) /\ exists ff_q_gcrt_dominating_solution_modulus. b = ff_q_gcrt_dominating_solution_modulus * S ((S (gcrt_solution_index_dominating_solution)) * c) + (gcrt_solution_modulus_dominating_solution))) -> (exists hgcrt_mod_left_gcrt_dominating_solution_congruence hgcrt_mod_right_gcrt_dominating_solution_congruence. a + gcrt_solution_modulus_dominating_solution * hgcrt_mod_left_gcrt_dominating_solution_congruence = gcrt_solution_residue_dominating_solution + gcrt_solution_modulus_dominating_solution * hgcrt_mod_right_gcrt_dominating_solution_congruence))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

63 script commands · 8 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 (1)
crt pairwise compatible prefix last

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–10

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 a
  7. L7
    intro M
  8. L8
    intro hpairs
  9. L9
    intro ha
  10. L10
    intro hM
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hcommon
03Use earlier factsL12–20

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

  1. L12
    specialize crt_prefix_solution_successor_intro r
  2. L13
    specialize crt_prefix_solution_successor_intro s
  3. L14
    specialize crt_prefix_solution_successor_intro b
  4. L15
    specialize crt_prefix_solution_successor_intro c
  5. L16
    specialize crt_prefix_solution_successor_intro l
  6. L17
    specialize crt_prefix_solution_successor_intro a
  7. L18
    specialize crt_prefix_solution_successor_intro a
  8. L19
    specialize crt_prefix_solution_successor_intro M
  9. L20
    apply crt_prefix_solution_successor_intro
04Fix variables and assumptionsL21–26

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

  1. L21
    intro i
  2. L22
    intro d
  3. L23
    intro m
  4. L24
    intro hi
  5. L25
    intro hd
  6. L26
    intro hm
05Establish hgL27–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply is gcd of dvd.

  1. L27
    have hg : IsGCD(m,m,M)Definitions: IsGCDOriginal native command in the exact edition
  2. L28
    specialize is_gcd_of_dvd m
  3. L29
    specialize is_gcd_of_dvd M
  4. L30
    apply is_gcd_of_dvd
  5. L31
    specialize hcommon i
  6. L32
    specialize hcommon m
  7. L33
    apply hcommon
  8. L34
    exact hi
  9. L35
    exact hm
  10. L36
    specialize mod_eq_symm m
06Use earlier factsL37–46

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

  1. L37
    specialize mod_eq_symm d
  2. L38
    specialize mod_eq_symm a
  3. L39
    apply mod_eq_symm
  4. L40
    specialize crt_pairwise_compatible_prefix_last r
  5. L41
    specialize crt_pairwise_compatible_prefix_last s
  6. L42
    specialize crt_pairwise_compatible_prefix_last b
  7. L43
    specialize crt_pairwise_compatible_prefix_last c
  8. L44
    specialize crt_pairwise_compatible_prefix_last l
  9. L45
    specialize crt_pairwise_compatible_prefix_last i
  10. L46
    specialize crt_pairwise_compatible_prefix_last d
07Use earlier factsL47–56

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

  1. L47
    specialize crt_pairwise_compatible_prefix_last a
  2. L48
    specialize crt_pairwise_compatible_prefix_last m
  3. L49
    specialize crt_pairwise_compatible_prefix_last M
  4. L50
    specialize crt_pairwise_compatible_prefix_last m
  5. L51
    apply crt_pairwise_compatible_prefix_last
  6. L52
    exact hpairs
  7. L53
    exact hi
  8. L54
    exact hd
  9. L55
    exact ha
  10. L56
    exact hm
08Use earlier factsL57–63

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

  1. L57
    exact hM
  2. L58
    exact hg
  3. L59
    exact ha
  4. L60
    exact hM
  5. L61
    specialize mod_eq_refl M
  6. L62
    specialize mod_eq_refl a
  7. L63
    exact mod_eq_refl

Library-wide reading audit

Original defined command ledger · 63 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro a
  7. 0007intro M
  8. 0008intro hpairs
  9. 0009intro ha
  10. 0010intro hM
  11. 0011intro hcommon
  12. 0012specialize crt_prefix_solution_successor_intro r
  13. 0013specialize crt_prefix_solution_successor_intro s
  14. 0014specialize crt_prefix_solution_successor_intro b
  15. 0015specialize crt_prefix_solution_successor_intro c
  16. 0016specialize crt_prefix_solution_successor_intro l
  17. 0017specialize crt_prefix_solution_successor_intro a
  18. 0018specialize crt_prefix_solution_successor_intro a
  19. 0019specialize crt_prefix_solution_successor_intro M
  20. 0020apply crt_prefix_solution_successor_intro
  21. 0021intro i
  22. 0022intro d
  23. 0023intro m
  24. 0024intro hi
  25. 0025intro hd
  26. 0026intro hm
  27. 0027have hg : (((exists hag_left_factor_gcomp_dominating_actual_gcd. m = m * hag_left_factor_gcomp_dominating_actual_gcd) /\ (exists hag_right_factor_gcomp_dominating_actual_gcd. M = m * hag_right_factor_gcomp_dominating_actual_gcd)) /\ forall hag_divisor_gcomp_dominating_actual_gcd. (exists hag_common_left_gcomp_dominating_actual_gcd. m = hag_divisor_gcomp_dominating_actual_gcd * hag_common_left_gcomp_dominating_actual_gcd) -> (exists hag_common_right_gcomp_dominating_actual_gcd. M = hag_divisor_gcomp_dominating_actual_gcd * hag_common_right_gcomp_dominating_actual_gcd) -> exists hag_greatest_factor_gcomp_dominating_actual_gcd. m = hag_divisor_gcomp_dominating_actual_gcd * hag_greatest_factor_gcomp_dominating_actual_gcd)
  28. 0028specialize is_gcd_of_dvd m
  29. 0029specialize is_gcd_of_dvd M
  30. 0030apply is_gcd_of_dvd
  31. 0031specialize hcommon i
  32. 0032specialize hcommon m
  33. 0033apply hcommon
  34. 0034exact hi
  35. 0035exact hm
  36. 0036specialize mod_eq_symm m
  37. 0037specialize mod_eq_symm d
  38. 0038specialize mod_eq_symm a
  39. 0039apply mod_eq_symm
  40. 0040specialize crt_pairwise_compatible_prefix_last r
  41. 0041specialize crt_pairwise_compatible_prefix_last s
  42. 0042specialize crt_pairwise_compatible_prefix_last b
  43. 0043specialize crt_pairwise_compatible_prefix_last c
  44. 0044specialize crt_pairwise_compatible_prefix_last l
  45. 0045specialize crt_pairwise_compatible_prefix_last i
  46. 0046specialize crt_pairwise_compatible_prefix_last d
  47. 0047specialize crt_pairwise_compatible_prefix_last a
  48. 0048specialize crt_pairwise_compatible_prefix_last m
  49. 0049specialize crt_pairwise_compatible_prefix_last M
  50. 0050specialize crt_pairwise_compatible_prefix_last m
  51. 0051apply crt_pairwise_compatible_prefix_last
  52. 0052exact hpairs
  53. 0053exact hi
  54. 0054exact hd
  55. 0055exact ha
  56. 0056exact hm
  57. 0057exact hM
  58. 0058exact hg
  59. 0059exact ha
  60. 0060exact hM
  61. 0061specialize mod_eq_refl M
  62. 0062specialize mod_eq_refl a
  63. 0063exact mod_eq_refl