FC000C

crt_pairwise_compatible_prefix_induces_gcd_congruences

Pairwise compatibility and an actual prefix solution imply every gcd congruence needed for the next merge, without any dominating-last or coprimality assumption.

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. ∀ i. ∀ x. ∀ a. ∀ n. CRTPairwiseCompatiblePrefix(r,s,b,c,l) → Lt(i,l) → CRTPrefixSolution(r,s,b,c,i,x) → BetaAt(r,s,i,a) → BetaAt(b,c,i,n) → CRTPrefixGcdCongruences(b,c,i,n,x,a)

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

Definition DAG

CRTPrefixSolution(r,s,b,c,l,x) · 1CRTPairwiseCompatiblePrefix(r,s,b,c,l) · 1CRTPrefixGcdCongruences(b,c,l,m,u,v) · 1Lt(a,b) · 1BetaAt(b,c,i,x) · 3

Actual proof prerequisites

beta_at_exists · checked external prerequisitelt_trans · checked external prerequisitemod_eq_trans · checked external prerequisitemod_eq_of_mod_eq_multiple · checked external prerequisiteis_gcd_dvd_left · checked external prerequisite
Original expanded first-order statement 
forall r s b c l i x a n. (forall gcomp_left_index_gfull_bridge_pairs gcomp_right_index_gfull_bridge_pairs gcomp_left_residue_gfull_bridge_pairs gcomp_right_residue_gfull_bridge_pairs gcomp_left_modulus_gfull_bridge_pairs gcomp_right_modulus_gfull_bridge_pairs gcomp_pair_gcd_gfull_bridge_pairs. (exists ff_lt_gcrt_gfull_bridge_pairs_left_bound. ff_lt_gcrt_gfull_bridge_pairs_left_bound + S gcomp_left_index_gfull_bridge_pairs = l) -> (exists ff_lt_gcrt_gfull_bridge_pairs_right_bound. ff_lt_gcrt_gfull_bridge_pairs_right_bound + S gcomp_right_index_gfull_bridge_pairs = l) -> (((exists ff_h_gcrt_gfull_bridge_pairs_left_residue. ff_h_gcrt_gfull_bridge_pairs_left_residue + S (gcomp_left_residue_gfull_bridge_pairs) = S ((S (gcomp_left_index_gfull_bridge_pairs)) * s)) /\ exists ff_q_gcrt_gfull_bridge_pairs_left_residue. r = ff_q_gcrt_gfull_bridge_pairs_left_residue * S ((S (gcomp_left_index_gfull_bridge_pairs)) * s) + (gcomp_left_residue_gfull_bridge_pairs))) -> (((exists ff_h_gcrt_gfull_bridge_pairs_right_residue. ff_h_gcrt_gfull_bridge_pairs_right_residue + S (gcomp_right_residue_gfull_bridge_pairs) = S ((S (gcomp_right_index_gfull_bridge_pairs)) * s)) /\ exists ff_q_gcrt_gfull_bridge_pairs_right_residue. r = ff_q_gcrt_gfull_bridge_pairs_right_residue * S ((S (gcomp_right_index_gfull_bridge_pairs)) * s) + (gcomp_right_residue_gfull_bridge_pairs))) -> (((exists ff_h_gcrt_gfull_bridge_pairs_left_modulus. ff_h_gcrt_gfull_bridge_pairs_left_modulus + S (gcomp_left_modulus_gfull_bridge_pairs) = S ((S (gcomp_left_index_gfull_bridge_pairs)) * c)) /\ exists ff_q_gcrt_gfull_bridge_pairs_left_modulus. b = ff_q_gcrt_gfull_bridge_pairs_left_modulus * S ((S (gcomp_left_index_gfull_bridge_pairs)) * c) + (gcomp_left_modulus_gfull_bridge_pairs))) -> (((exists ff_h_gcrt_gfull_bridge_pairs_right_modulus. ff_h_gcrt_gfull_bridge_pairs_right_modulus + S (gcomp_right_modulus_gfull_bridge_pairs) = S ((S (gcomp_right_index_gfull_bridge_pairs)) * c)) /\ exists ff_q_gcrt_gfull_bridge_pairs_right_modulus. b = ff_q_gcrt_gfull_bridge_pairs_right_modulus * S ((S (gcomp_right_index_gfull_bridge_pairs)) * c) + (gcomp_right_modulus_gfull_bridge_pairs))) -> ((((exists hag_left_factor_gcomp_gfull_bridge_pairs_gcd. gcomp_left_modulus_gfull_bridge_pairs = gcomp_pair_gcd_gfull_bridge_pairs * hag_left_factor_gcomp_gfull_bridge_pairs_gcd) /\ (exists hag_right_factor_gcomp_gfull_bridge_pairs_gcd. gcomp_right_modulus_gfull_bridge_pairs = gcomp_pair_gcd_gfull_bridge_pairs * hag_right_factor_gcomp_gfull_bridge_pairs_gcd)) /\ forall hag_divisor_gcomp_gfull_bridge_pairs_gcd. (exists hag_common_left_gcomp_gfull_bridge_pairs_gcd. gcomp_left_modulus_gfull_bridge_pairs = hag_divisor_gcomp_gfull_bridge_pairs_gcd * hag_common_left_gcomp_gfull_bridge_pairs_gcd) -> (exists hag_common_right_gcomp_gfull_bridge_pairs_gcd. gcomp_right_modulus_gfull_bridge_pairs = hag_divisor_gcomp_gfull_bridge_pairs_gcd * hag_common_right_gcomp_gfull_bridge_pairs_gcd) -> exists hag_greatest_factor_gcomp_gfull_bridge_pairs_gcd. gcomp_pair_gcd_gfull_bridge_pairs = hag_divisor_gcomp_gfull_bridge_pairs_gcd * hag_greatest_factor_gcomp_gfull_bridge_pairs_gcd)) -> (exists hgcrt_mod_left_gcrt_gfull_bridge_pairs_result hgcrt_mod_right_gcrt_gfull_bridge_pairs_result. gcomp_left_residue_gfull_bridge_pairs + gcomp_pair_gcd_gfull_bridge_pairs * hgcrt_mod_left_gcrt_gfull_bridge_pairs_result = gcomp_right_residue_gfull_bridge_pairs + gcomp_pair_gcd_gfull_bridge_pairs * hgcrt_mod_right_gcrt_gfull_bridge_pairs_result)) -> (exists ff_lt_gcrt_gfull_bridge_index. ff_lt_gcrt_gfull_bridge_index + S i = l) -> (forall gcrt_solution_index_gfull_bridge_solution gcrt_solution_residue_gfull_bridge_solution gcrt_solution_modulus_gfull_bridge_solution. (exists ff_lt_gcrt_gfull_bridge_solution_bound. ff_lt_gcrt_gfull_bridge_solution_bound + S gcrt_solution_index_gfull_bridge_solution = i) -> (((exists ff_h_gcrt_gfull_bridge_solution_residue. ff_h_gcrt_gfull_bridge_solution_residue + S (gcrt_solution_residue_gfull_bridge_solution) = S ((S (gcrt_solution_index_gfull_bridge_solution)) * s)) /\ exists ff_q_gcrt_gfull_bridge_solution_residue. r = ff_q_gcrt_gfull_bridge_solution_residue * S ((S (gcrt_solution_index_gfull_bridge_solution)) * s) + (gcrt_solution_residue_gfull_bridge_solution))) -> (((exists ff_h_gcrt_gfull_bridge_solution_modulus. ff_h_gcrt_gfull_bridge_solution_modulus + S (gcrt_solution_modulus_gfull_bridge_solution) = S ((S (gcrt_solution_index_gfull_bridge_solution)) * c)) /\ exists ff_q_gcrt_gfull_bridge_solution_modulus. b = ff_q_gcrt_gfull_bridge_solution_modulus * S ((S (gcrt_solution_index_gfull_bridge_solution)) * c) + (gcrt_solution_modulus_gfull_bridge_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_bridge_solution_congruence hgcrt_mod_right_gcrt_gfull_bridge_solution_congruence. x + gcrt_solution_modulus_gfull_bridge_solution * hgcrt_mod_left_gcrt_gfull_bridge_solution_congruence = gcrt_solution_residue_gfull_bridge_solution + gcrt_solution_modulus_gfull_bridge_solution * hgcrt_mod_right_gcrt_gfull_bridge_solution_congruence)) -> (((exists ff_h_gcrt_gfull_bridge_residue. ff_h_gcrt_gfull_bridge_residue + S (a) = S ((S (i)) * s)) /\ exists ff_q_gcrt_gfull_bridge_residue. r = ff_q_gcrt_gfull_bridge_residue * S ((S (i)) * s) + (a))) -> (((exists ff_h_gcrt_gfull_bridge_modulus. ff_h_gcrt_gfull_bridge_modulus + S (n) = S ((S (i)) * c)) /\ exists ff_q_gcrt_gfull_bridge_modulus. b = ff_q_gcrt_gfull_bridge_modulus * S ((S (i)) * c) + (n))) -> (forall gfull_index_bridge_result gfull_modulus_bridge_result gfull_gcd_bridge_result. (exists ff_lt_gcrt_gfull_bridge_result_bound. ff_lt_gcrt_gfull_bridge_result_bound + S gfull_index_bridge_result = i) -> (((exists ff_h_gcrt_gfull_bridge_result_entry. ff_h_gcrt_gfull_bridge_result_entry + S (gfull_modulus_bridge_result) = S ((S (gfull_index_bridge_result)) * c)) /\ exists ff_q_gcrt_gfull_bridge_result_entry. b = ff_q_gcrt_gfull_bridge_result_entry * S ((S (gfull_index_bridge_result)) * c) + (gfull_modulus_bridge_result))) -> ((((exists ec_gcd_left_gfull_bridge_result_gcd. gfull_modulus_bridge_result = gfull_gcd_bridge_result * ec_gcd_left_gfull_bridge_result_gcd) /\ (exists ec_gcd_right_gfull_bridge_result_gcd. n = gfull_gcd_bridge_result * ec_gcd_right_gfull_bridge_result_gcd)) /\ forall ec_gcd_common_gfull_bridge_result_gcd. (exists ec_gcd_common_left_gfull_bridge_result_gcd. gfull_modulus_bridge_result = ec_gcd_common_gfull_bridge_result_gcd * ec_gcd_common_left_gfull_bridge_result_gcd) -> (exists ec_gcd_common_right_gfull_bridge_result_gcd. n = ec_gcd_common_gfull_bridge_result_gcd * ec_gcd_common_right_gfull_bridge_result_gcd) -> exists ec_gcd_greatest_gfull_bridge_result_gcd. gfull_gcd_bridge_result = ec_gcd_common_gfull_bridge_result_gcd * ec_gcd_greatest_gfull_bridge_result_gcd)) -> (exists hgcrt_mod_left_gfull_bridge_result_mod hgcrt_mod_right_gfull_bridge_result_mod. x + gfull_gcd_bridge_result * hgcrt_mod_left_gfull_bridge_result_mod = a + gfull_gcd_bridge_result * hgcrt_mod_right_gfull_bridge_result_mod))

Complete tactic proof in conservative notation

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

68 script commands · 9 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.

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 i
  7. L7
    intro x
  8. L8
    intro a
  9. L9
    intro n
  10. L10
    intro hp
02Fix variables and assumptionsL11–20

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

  1. L11
    intro hi
  2. L12
    intro hs
  3. L13
    intro ha
  4. L14
    intro hn
  5. L15
    intro j
  6. L16
    intro m
  7. L17
    intro d
  8. L18
    intro hj
  9. L19
    intro hm
  10. L20
    intro hd
03Establish hzL21–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at exists.

  1. L21
    have hz : ∃ z. BetaAt(r,s,j,z)Definitions: BetaAt(r,s,j,z)Original native command in the exact edition
  2. L22
    specialize beta_at_exists r
  3. L23
    specialize beta_at_exists s
  4. L24
    specialize beta_at_exists j
  5. L25
    apply beta_at_exists
04Separate the logical casesL26–26

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

  1. L26
    cases hz
05Use earlier factsL27–36

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

  1. L27
    specialize mod_eq_trans d
  2. L28
    specialize mod_eq_trans x
  3. L29
    specialize mod_eq_trans x1
  4. L30
    specialize mod_eq_trans a
  5. L31
    apply mod_eq_trans
  6. L32
    specialize mod_eq_of_mod_eq_multiple d
  7. L33
    specialize mod_eq_of_mod_eq_multiple m
  8. L34
    specialize mod_eq_of_mod_eq_multiple x
  9. L35
    specialize mod_eq_of_mod_eq_multiple x1
  10. L36
    apply mod_eq_of_mod_eq_multiple
06Use earlier factsL37–46

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

  1. L37
    specialize is_gcd_dvd_left d
  2. L38
    specialize is_gcd_dvd_left m
  3. L39
    specialize is_gcd_dvd_left n
  4. L40
    apply is_gcd_dvd_left
  5. L41
    exact hd
  6. L42
    specialize hs j
  7. L43
    specialize hs x1
  8. L44
    specialize hs m
  9. L45
    apply hs
  10. L46
    exact hj
07Use earlier factsL47–56

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

  1. L47
    exact hz_witness
  2. L48
    exact hm
  3. L49
    specialize hp j
  4. L50
    specialize hp i
  5. L51
    specialize hp x1
  6. L52
    specialize hp a
  7. L53
    specialize hp m
  8. L54
    specialize hp n
  9. L55
    specialize hp d
  10. L56
    apply hp
08Use earlier factsL57–66

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

  1. L57
    specialize lt_trans j
  2. L58
    specialize lt_trans i
  3. L59
    specialize lt_trans l
  4. L60
    apply lt_trans
  5. L61
    exact hj
  6. L62
    exact hi
  7. L63
    exact hi
  8. L64
    exact hz_witness
  9. L65
    exact ha
  10. L66
    exact hm
09Use earlier factsL67–68

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

  1. L67
    exact hn
  2. L68
    exact hd

Library-wide reading audit

Original defined command ledger · 68 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro i
  7. 0007intro x
  8. 0008intro a
  9. 0009intro n
  10. 0010intro hp
  11. 0011intro hi
  12. 0012intro hs
  13. 0013intro ha
  14. 0014intro hn
  15. 0015intro j
  16. 0016intro m
  17. 0017intro d
  18. 0018intro hj
  19. 0019intro hm
  20. 0020intro hd
  21. 0021have hz : ∃ z. BetaAt(r,s,j,z)
  22. 0022specialize beta_at_exists r
  23. 0023specialize beta_at_exists s
  24. 0024specialize beta_at_exists j
  25. 0025apply beta_at_exists
  26. 0026cases hz
  27. 0027specialize mod_eq_trans d
  28. 0028specialize mod_eq_trans x
  29. 0029specialize mod_eq_trans x1
  30. 0030specialize mod_eq_trans a
  31. 0031apply mod_eq_trans
  32. 0032specialize mod_eq_of_mod_eq_multiple d
  33. 0033specialize mod_eq_of_mod_eq_multiple m
  34. 0034specialize mod_eq_of_mod_eq_multiple x
  35. 0035specialize mod_eq_of_mod_eq_multiple x1
  36. 0036apply mod_eq_of_mod_eq_multiple
  37. 0037specialize is_gcd_dvd_left d
  38. 0038specialize is_gcd_dvd_left m
  39. 0039specialize is_gcd_dvd_left n
  40. 0040apply is_gcd_dvd_left
  41. 0041exact hd
  42. 0042specialize hs j
  43. 0043specialize hs x1
  44. 0044specialize hs m
  45. 0045apply hs
  46. 0046exact hj
  47. 0047exact hz_witness
  48. 0048exact hm
  49. 0049specialize hp j
  50. 0050specialize hp i
  51. 0051specialize hp x1
  52. 0052specialize hp a
  53. 0053specialize hp m
  54. 0054specialize hp n
  55. 0055specialize hp d
  56. 0056apply hp
  57. 0057specialize lt_trans j
  58. 0058specialize lt_trans i
  59. 0059specialize lt_trans l
  60. 0060apply lt_trans
  61. 0061exact hj
  62. 0062exact hi
  63. 0063exact hi
  64. 0064exact hz_witness
  65. 0065exact ha
  66. 0066exact hm
  67. 0067exact hn
  68. 0068exact hd