CR0017

crt_prefix_solutions_congruent_lcm

For arbitrary decoded lists, every two simultaneous solutions are congruent modulo the exact list lcm.

Alpha v34 checked-use · first admitted v24 · 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 for finite positive pairwise-coprime systems and exact LCM solution classes. G011 is now closed in the separate Alpha-v27 generalized-crt branch for arbitrary pairwise-compatible systems, including noncoprime moduli. Full G011 proof · Alpha v27

Exact theorem in conservative defined notation

∀ r. ∀ s. ∀ b. ∀ c. ∀ l. ∀ M. ∀ x. ∀ y. CRTPrefixLCM(b,c,l,M) → CRTPrefixSolution(r,s,b,c,l,x) → CRTPrefixSolution(r,s,b,c,l,y) → ModEq(M,x,y)

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

Definition DAG

CRTPrefixSolution(r,s,b,c,l,x) · 2CRTPrefixLCM(b,c,l,M) · 1ModEq(m,a,b) · 1

Actual proof prerequisites

le_total · checked external prerequisitecrt_prefix_ordered_solutions_gap_multipleremainder_decomposition_to_mod_eq · checked external prerequisitemul_comm · checked external prerequisitemod_eq_symm · checked external prerequisite
Original expanded first-order statement 
forall r s b c l M x y. (((forall gcrt_common_index_class_lcm_own gcrt_common_modulus_class_lcm_own. (exists ff_lt_gcrt_class_lcm_own_bound. ff_lt_gcrt_class_lcm_own_bound + S gcrt_common_index_class_lcm_own = l) -> (((exists ff_h_gcrt_class_lcm_own_entry. ff_h_gcrt_class_lcm_own_entry + S (gcrt_common_modulus_class_lcm_own) = S ((S (gcrt_common_index_class_lcm_own)) * c)) /\ exists ff_q_gcrt_class_lcm_own_entry. b = ff_q_gcrt_class_lcm_own_entry * S ((S (gcrt_common_index_class_lcm_own)) * c) + (gcrt_common_modulus_class_lcm_own))) -> exists gcrt_common_quotient_class_lcm_own. M = gcrt_common_modulus_class_lcm_own * gcrt_common_quotient_class_lcm_own) /\ forall gcrt_lcm_common_class_lcm. (forall gcrt_common_index_class_lcm_other gcrt_common_modulus_class_lcm_other. (exists ff_lt_gcrt_class_lcm_other_bound. ff_lt_gcrt_class_lcm_other_bound + S gcrt_common_index_class_lcm_other = l) -> (((exists ff_h_gcrt_class_lcm_other_entry. ff_h_gcrt_class_lcm_other_entry + S (gcrt_common_modulus_class_lcm_other) = S ((S (gcrt_common_index_class_lcm_other)) * c)) /\ exists ff_q_gcrt_class_lcm_other_entry. b = ff_q_gcrt_class_lcm_other_entry * S ((S (gcrt_common_index_class_lcm_other)) * c) + (gcrt_common_modulus_class_lcm_other))) -> exists gcrt_common_quotient_class_lcm_other. gcrt_lcm_common_class_lcm = gcrt_common_modulus_class_lcm_other * gcrt_common_quotient_class_lcm_other) -> exists gcrt_lcm_quotient_class_lcm. gcrt_lcm_common_class_lcm = M * gcrt_lcm_quotient_class_lcm)) -> (forall gcrt_solution_index_class_solution_left gcrt_solution_residue_class_solution_left gcrt_solution_modulus_class_solution_left. (exists ff_lt_gcrt_class_solution_left_bound. ff_lt_gcrt_class_solution_left_bound + S gcrt_solution_index_class_solution_left = l) -> (((exists ff_h_gcrt_class_solution_left_residue. ff_h_gcrt_class_solution_left_residue + S (gcrt_solution_residue_class_solution_left) = S ((S (gcrt_solution_index_class_solution_left)) * s)) /\ exists ff_q_gcrt_class_solution_left_residue. r = ff_q_gcrt_class_solution_left_residue * S ((S (gcrt_solution_index_class_solution_left)) * s) + (gcrt_solution_residue_class_solution_left))) -> (((exists ff_h_gcrt_class_solution_left_modulus. ff_h_gcrt_class_solution_left_modulus + S (gcrt_solution_modulus_class_solution_left) = S ((S (gcrt_solution_index_class_solution_left)) * c)) /\ exists ff_q_gcrt_class_solution_left_modulus. b = ff_q_gcrt_class_solution_left_modulus * S ((S (gcrt_solution_index_class_solution_left)) * c) + (gcrt_solution_modulus_class_solution_left))) -> (exists hgcrt_mod_left_gcrt_class_solution_left_congruence hgcrt_mod_right_gcrt_class_solution_left_congruence. x + gcrt_solution_modulus_class_solution_left * hgcrt_mod_left_gcrt_class_solution_left_congruence = gcrt_solution_residue_class_solution_left + gcrt_solution_modulus_class_solution_left * hgcrt_mod_right_gcrt_class_solution_left_congruence)) -> (forall gcrt_solution_index_class_solution_right gcrt_solution_residue_class_solution_right gcrt_solution_modulus_class_solution_right. (exists ff_lt_gcrt_class_solution_right_bound. ff_lt_gcrt_class_solution_right_bound + S gcrt_solution_index_class_solution_right = l) -> (((exists ff_h_gcrt_class_solution_right_residue. ff_h_gcrt_class_solution_right_residue + S (gcrt_solution_residue_class_solution_right) = S ((S (gcrt_solution_index_class_solution_right)) * s)) /\ exists ff_q_gcrt_class_solution_right_residue. r = ff_q_gcrt_class_solution_right_residue * S ((S (gcrt_solution_index_class_solution_right)) * s) + (gcrt_solution_residue_class_solution_right))) -> (((exists ff_h_gcrt_class_solution_right_modulus. ff_h_gcrt_class_solution_right_modulus + S (gcrt_solution_modulus_class_solution_right) = S ((S (gcrt_solution_index_class_solution_right)) * c)) /\ exists ff_q_gcrt_class_solution_right_modulus. b = ff_q_gcrt_class_solution_right_modulus * S ((S (gcrt_solution_index_class_solution_right)) * c) + (gcrt_solution_modulus_class_solution_right))) -> (exists hgcrt_mod_left_gcrt_class_solution_right_congruence hgcrt_mod_right_gcrt_class_solution_right_congruence. y + gcrt_solution_modulus_class_solution_right * hgcrt_mod_left_gcrt_class_solution_right_congruence = gcrt_solution_residue_class_solution_right + gcrt_solution_modulus_class_solution_right * hgcrt_mod_right_gcrt_class_solution_right_congruence)) -> (exists hgcrt_mod_left_gcrt_class_result hgcrt_mod_right_gcrt_class_result. x + M * hgcrt_mod_left_gcrt_class_result = y + M * hgcrt_mod_right_gcrt_class_result)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

78 script commands · 22 reading checkpoints · 3 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 prefix ordered solutions gap multiple
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 M
  7. L7
    intro x
  8. L8
    intro y
  9. L9
    intro hlcm
  10. L10
    intro hx
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hy
03Use earlier factsL12–13

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

  1. L12
    specialize le_total x
  2. L13
    specialize le_total y
04Separate the logical casesL14–15

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

  1. L14
    cases le_total
  2. L15
    cases le_total_left
05Establish hgapL16–25

Establish this local claim before using it. It is not an additional assumption.

  1. L16
    have hgap : exists q. x1 = M * q
  2. L17
    specialize crt_prefix_ordered_solutions_gap_multiple r
  3. L18
    specialize crt_prefix_ordered_solutions_gap_multiple s
  4. L19
    specialize crt_prefix_ordered_solutions_gap_multiple b
  5. L20
    specialize crt_prefix_ordered_solutions_gap_multiple c
  6. L21
    specialize crt_prefix_ordered_solutions_gap_multiple l
  7. L22
    specialize crt_prefix_ordered_solutions_gap_multiple M
  8. L23
    specialize crt_prefix_ordered_solutions_gap_multiple x
  9. L24
    specialize crt_prefix_ordered_solutions_gap_multiple y
  10. L25
    specialize crt_prefix_ordered_solutions_gap_multiple x1
06Use earlier factsL26–30

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

  1. L26
    apply crt_prefix_ordered_solutions_gap_multiple
  2. L27
    exact hlcm
  3. L28
    exact hx
  4. L29
    exact hy
  5. L30
    exact le_total_left_witness
07Separate the logical casesL31–31

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

  1. L31
    cases hgap
08Establish hreverseL32–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply remainder decomposition to mod eq.

  1. L32
    have hreverse : exists hgcrt_mod_left_gcrt_class_reverse hgcrt_mod_right_gcrt_class_reverse. y + M * hgcrt_mod_left_gcrt_class_reverse = x + M * hgcrt_mod_right_gcrt_class_reverse
  2. L33
    specialize remainder_decomposition_to_mod_eq M
  3. L34
    specialize remainder_decomposition_to_mod_eq y
  4. L35
    specialize remainder_decomposition_to_mod_eq x2
  5. L36
    specialize remainder_decomposition_to_mod_eq x
  6. L37
    apply remainder_decomposition_to_mod_eq
  7. L38
    trans x1 + x
  8. L39
    symm
  9. L40
    exact le_total_left_witness
  10. L41
    rewrite hgap_witness
09Calculate and transport equalitiesL42–42

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L42
    congr
10Use earlier factsL43–43

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

  1. L43
    apply mul_comm
11Calculate and transport equalitiesL44–44

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L44
    refl
12Use earlier factsL45–49

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

  1. L45
    specialize mod_eq_symm M
  2. L46
    specialize mod_eq_symm y
  3. L47
    specialize mod_eq_symm x
  4. L48
    apply mod_eq_symm
  5. L49
    exact hreverse
13Separate the logical casesL50–50

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

  1. L50
    cases le_total_right
14Establish hgapL51–60

Establish this local claim before using it. It is not an additional assumption.

  1. L51
    have hgap : exists q. x1 = M * q
  2. L52
    specialize crt_prefix_ordered_solutions_gap_multiple r
  3. L53
    specialize crt_prefix_ordered_solutions_gap_multiple s
  4. L54
    specialize crt_prefix_ordered_solutions_gap_multiple b
  5. L55
    specialize crt_prefix_ordered_solutions_gap_multiple c
  6. L56
    specialize crt_prefix_ordered_solutions_gap_multiple l
  7. L57
    specialize crt_prefix_ordered_solutions_gap_multiple M
  8. L58
    specialize crt_prefix_ordered_solutions_gap_multiple y
  9. L59
    specialize crt_prefix_ordered_solutions_gap_multiple x
  10. L60
    specialize crt_prefix_ordered_solutions_gap_multiple x1
15Use earlier factsL61–65

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

  1. L61
    apply crt_prefix_ordered_solutions_gap_multiple
  2. L62
    exact hlcm
  3. L63
    exact hy
  4. L64
    exact hx
  5. L65
    exact le_total_right_witness
16Separate the logical casesL66–66

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

  1. L66
    cases hgap
17Use earlier factsL67–71

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

  1. L67
    specialize remainder_decomposition_to_mod_eq M
  2. L68
    specialize remainder_decomposition_to_mod_eq x
  3. L69
    specialize remainder_decomposition_to_mod_eq x2
  4. L70
    specialize remainder_decomposition_to_mod_eq y
  5. L71
    apply remainder_decomposition_to_mod_eq
18Calculate and transport equalitiesL72–73

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L72
    trans x1 + y
  2. L73
    symm
19Use earlier factsL74–74

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

  1. L74
    exact le_total_right_witness
20Calculate and transport equalitiesL75–76

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L75
    rewrite hgap_witness
  2. L76
    congr
21Use earlier factsL77–77

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

  1. L77
    apply mul_comm
22Calculate and transport equalitiesL78–78

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L78
    refl

Library-wide reading audit

Original defined command ledger · 78 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro M
  7. 0007intro x
  8. 0008intro y
  9. 0009intro hlcm
  10. 0010intro hx
  11. 0011intro hy
  12. 0012specialize le_total x
  13. 0013specialize le_total y
  14. 0014cases le_total
  15. 0015cases le_total_left
  16. 0016have hgap : exists q. x1 = M * q
  17. 0017specialize crt_prefix_ordered_solutions_gap_multiple r
  18. 0018specialize crt_prefix_ordered_solutions_gap_multiple s
  19. 0019specialize crt_prefix_ordered_solutions_gap_multiple b
  20. 0020specialize crt_prefix_ordered_solutions_gap_multiple c
  21. 0021specialize crt_prefix_ordered_solutions_gap_multiple l
  22. 0022specialize crt_prefix_ordered_solutions_gap_multiple M
  23. 0023specialize crt_prefix_ordered_solutions_gap_multiple x
  24. 0024specialize crt_prefix_ordered_solutions_gap_multiple y
  25. 0025specialize crt_prefix_ordered_solutions_gap_multiple x1
  26. 0026apply crt_prefix_ordered_solutions_gap_multiple
  27. 0027exact hlcm
  28. 0028exact hx
  29. 0029exact hy
  30. 0030exact le_total_left_witness
  31. 0031cases hgap
  32. 0032have hreverse : exists hgcrt_mod_left_gcrt_class_reverse hgcrt_mod_right_gcrt_class_reverse. y + M * hgcrt_mod_left_gcrt_class_reverse = x + M * hgcrt_mod_right_gcrt_class_reverse
  33. 0033specialize remainder_decomposition_to_mod_eq M
  34. 0034specialize remainder_decomposition_to_mod_eq y
  35. 0035specialize remainder_decomposition_to_mod_eq x2
  36. 0036specialize remainder_decomposition_to_mod_eq x
  37. 0037apply remainder_decomposition_to_mod_eq
  38. 0038trans x1 + x
  39. 0039symm
  40. 0040exact le_total_left_witness
  41. 0041rewrite hgap_witness
  42. 0042congr
  43. 0043apply mul_comm
  44. 0044refl
  45. 0045specialize mod_eq_symm M
  46. 0046specialize mod_eq_symm y
  47. 0047specialize mod_eq_symm x
  48. 0048apply mod_eq_symm
  49. 0049exact hreverse
  50. 0050cases le_total_right
  51. 0051have hgap : exists q. x1 = M * q
  52. 0052specialize crt_prefix_ordered_solutions_gap_multiple r
  53. 0053specialize crt_prefix_ordered_solutions_gap_multiple s
  54. 0054specialize crt_prefix_ordered_solutions_gap_multiple b
  55. 0055specialize crt_prefix_ordered_solutions_gap_multiple c
  56. 0056specialize crt_prefix_ordered_solutions_gap_multiple l
  57. 0057specialize crt_prefix_ordered_solutions_gap_multiple M
  58. 0058specialize crt_prefix_ordered_solutions_gap_multiple y
  59. 0059specialize crt_prefix_ordered_solutions_gap_multiple x
  60. 0060specialize crt_prefix_ordered_solutions_gap_multiple x1
  61. 0061apply crt_prefix_ordered_solutions_gap_multiple
  62. 0062exact hlcm
  63. 0063exact hy
  64. 0064exact hx
  65. 0065exact le_total_right_witness
  66. 0066cases hgap
  67. 0067specialize remainder_decomposition_to_mod_eq M
  68. 0068specialize remainder_decomposition_to_mod_eq x
  69. 0069specialize remainder_decomposition_to_mod_eq x2
  70. 0070specialize remainder_decomposition_to_mod_eq y
  71. 0071apply remainder_decomposition_to_mod_eq
  72. 0072trans x1 + y
  73. 0073symm
  74. 0074exact le_total_right_witness
  75. 0075rewrite hgap_witness
  76. 0076congr
  77. 0077apply mul_comm
  78. 0078refl