CR0016

crt_prefix_ordered_solutions_gap_multiple

For every finite list, the directed gap between two solutions is divisible by its universal-property 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. ∀ k. CRTPrefixLCM(b,c,l,M) → CRTPrefixSolution(r,s,b,c,l,x) → CRTPrefixSolution(r,s,b,c,l,y) → k + x = y → Dvd(M,k)

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) · 1Dvd(d,n) · 1

Actual proof prerequisites

beta_at_exists · checked external prerequisitecrt_prefix_solutions_pointwise_congruentmod_eq_ordered_gap_multiple · checked external prerequisite
Original expanded first-order statement 
forall r s b c l M x y k. (((forall gcrt_common_index_gap_lcm_own gcrt_common_modulus_gap_lcm_own. (exists ff_lt_gcrt_gap_lcm_own_bound. ff_lt_gcrt_gap_lcm_own_bound + S gcrt_common_index_gap_lcm_own = l) -> (((exists ff_h_gcrt_gap_lcm_own_entry. ff_h_gcrt_gap_lcm_own_entry + S (gcrt_common_modulus_gap_lcm_own) = S ((S (gcrt_common_index_gap_lcm_own)) * c)) /\ exists ff_q_gcrt_gap_lcm_own_entry. b = ff_q_gcrt_gap_lcm_own_entry * S ((S (gcrt_common_index_gap_lcm_own)) * c) + (gcrt_common_modulus_gap_lcm_own))) -> exists gcrt_common_quotient_gap_lcm_own. M = gcrt_common_modulus_gap_lcm_own * gcrt_common_quotient_gap_lcm_own) /\ forall gcrt_lcm_common_gap_lcm. (forall gcrt_common_index_gap_lcm_other gcrt_common_modulus_gap_lcm_other. (exists ff_lt_gcrt_gap_lcm_other_bound. ff_lt_gcrt_gap_lcm_other_bound + S gcrt_common_index_gap_lcm_other = l) -> (((exists ff_h_gcrt_gap_lcm_other_entry. ff_h_gcrt_gap_lcm_other_entry + S (gcrt_common_modulus_gap_lcm_other) = S ((S (gcrt_common_index_gap_lcm_other)) * c)) /\ exists ff_q_gcrt_gap_lcm_other_entry. b = ff_q_gcrt_gap_lcm_other_entry * S ((S (gcrt_common_index_gap_lcm_other)) * c) + (gcrt_common_modulus_gap_lcm_other))) -> exists gcrt_common_quotient_gap_lcm_other. gcrt_lcm_common_gap_lcm = gcrt_common_modulus_gap_lcm_other * gcrt_common_quotient_gap_lcm_other) -> exists gcrt_lcm_quotient_gap_lcm. gcrt_lcm_common_gap_lcm = M * gcrt_lcm_quotient_gap_lcm)) -> (forall gcrt_solution_index_gap_solution_left gcrt_solution_residue_gap_solution_left gcrt_solution_modulus_gap_solution_left. (exists ff_lt_gcrt_gap_solution_left_bound. ff_lt_gcrt_gap_solution_left_bound + S gcrt_solution_index_gap_solution_left = l) -> (((exists ff_h_gcrt_gap_solution_left_residue. ff_h_gcrt_gap_solution_left_residue + S (gcrt_solution_residue_gap_solution_left) = S ((S (gcrt_solution_index_gap_solution_left)) * s)) /\ exists ff_q_gcrt_gap_solution_left_residue. r = ff_q_gcrt_gap_solution_left_residue * S ((S (gcrt_solution_index_gap_solution_left)) * s) + (gcrt_solution_residue_gap_solution_left))) -> (((exists ff_h_gcrt_gap_solution_left_modulus. ff_h_gcrt_gap_solution_left_modulus + S (gcrt_solution_modulus_gap_solution_left) = S ((S (gcrt_solution_index_gap_solution_left)) * c)) /\ exists ff_q_gcrt_gap_solution_left_modulus. b = ff_q_gcrt_gap_solution_left_modulus * S ((S (gcrt_solution_index_gap_solution_left)) * c) + (gcrt_solution_modulus_gap_solution_left))) -> (exists hgcrt_mod_left_gcrt_gap_solution_left_congruence hgcrt_mod_right_gcrt_gap_solution_left_congruence. x + gcrt_solution_modulus_gap_solution_left * hgcrt_mod_left_gcrt_gap_solution_left_congruence = gcrt_solution_residue_gap_solution_left + gcrt_solution_modulus_gap_solution_left * hgcrt_mod_right_gcrt_gap_solution_left_congruence)) -> (forall gcrt_solution_index_gap_solution_right gcrt_solution_residue_gap_solution_right gcrt_solution_modulus_gap_solution_right. (exists ff_lt_gcrt_gap_solution_right_bound. ff_lt_gcrt_gap_solution_right_bound + S gcrt_solution_index_gap_solution_right = l) -> (((exists ff_h_gcrt_gap_solution_right_residue. ff_h_gcrt_gap_solution_right_residue + S (gcrt_solution_residue_gap_solution_right) = S ((S (gcrt_solution_index_gap_solution_right)) * s)) /\ exists ff_q_gcrt_gap_solution_right_residue. r = ff_q_gcrt_gap_solution_right_residue * S ((S (gcrt_solution_index_gap_solution_right)) * s) + (gcrt_solution_residue_gap_solution_right))) -> (((exists ff_h_gcrt_gap_solution_right_modulus. ff_h_gcrt_gap_solution_right_modulus + S (gcrt_solution_modulus_gap_solution_right) = S ((S (gcrt_solution_index_gap_solution_right)) * c)) /\ exists ff_q_gcrt_gap_solution_right_modulus. b = ff_q_gcrt_gap_solution_right_modulus * S ((S (gcrt_solution_index_gap_solution_right)) * c) + (gcrt_solution_modulus_gap_solution_right))) -> (exists hgcrt_mod_left_gcrt_gap_solution_right_congruence hgcrt_mod_right_gcrt_gap_solution_right_congruence. y + gcrt_solution_modulus_gap_solution_right * hgcrt_mod_left_gcrt_gap_solution_right_congruence = gcrt_solution_residue_gap_solution_right + gcrt_solution_modulus_gap_solution_right * hgcrt_mod_right_gcrt_gap_solution_right_congruence)) -> k + x = y -> exists q. k = M * q

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

48 script commands · 10 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 prefix solutions pointwise congruent
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 k
  10. L10
    intro hlcm
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hx
  2. L12
    intro hy
  3. L13
    intro hgap
03Separate the logical casesL14–14

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

  1. L14
    cases hlcm
04Use earlier factsL15–16

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

  1. L15
    specialize hlcm_right k
  2. L16
    apply hlcm_right
05Fix variables and assumptionsL17–20

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

  1. L17
    intro i
  2. L18
    intro m
  3. L19
    intro hi
  4. L20
    intro hm
06Establish hresidueL21–25

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

  1. L21
    have hresidue : exists a. (((exists ff_h_gcrt_gap_decoded_residue. ff_h_gcrt_gap_decoded_residue + S (a) = S ((S (i)) * s)) /\ exists ff_q_gcrt_gap_decoded_residue. r = ff_q_gcrt_gap_decoded_residue * S ((S (i)) * s) + (a)))
  2. L22
    specialize beta_at_exists r
  3. L23
    specialize beta_at_exists s
  4. L24
    specialize beta_at_exists i
  5. L25
    exact beta_at_exists
07Separate the logical casesL26–26

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

  1. L26
    cases hresidue
08Use earlier factsL27–36

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

  1. L27
    specialize mod_eq_ordered_gap_multiple m
  2. L28
    specialize mod_eq_ordered_gap_multiple k
  3. L29
    specialize mod_eq_ordered_gap_multiple x
  4. L30
    specialize mod_eq_ordered_gap_multiple y
  5. L31
    apply mod_eq_ordered_gap_multiple
  6. L32
    exact hgap
  7. L33
    specialize crt_prefix_solutions_pointwise_congruent r
  8. L34
    specialize crt_prefix_solutions_pointwise_congruent s
  9. L35
    specialize crt_prefix_solutions_pointwise_congruent b
  10. L36
    specialize crt_prefix_solutions_pointwise_congruent c
09Use earlier factsL37–46

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

  1. L37
    specialize crt_prefix_solutions_pointwise_congruent l
  2. L38
    specialize crt_prefix_solutions_pointwise_congruent x
  3. L39
    specialize crt_prefix_solutions_pointwise_congruent y
  4. L40
    specialize crt_prefix_solutions_pointwise_congruent i
  5. L41
    specialize crt_prefix_solutions_pointwise_congruent x1
  6. L42
    specialize crt_prefix_solutions_pointwise_congruent m
  7. L43
    apply crt_prefix_solutions_pointwise_congruent
  8. L44
    exact hx
  9. L45
    exact hy
  10. L46
    exact hi
10Use earlier factsL47–48

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

  1. L47
    exact hresidue_witness
  2. L48
    exact hm

Library-wide reading audit

Original defined command ledger · 48 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 k
  10. 0010intro hlcm
  11. 0011intro hx
  12. 0012intro hy
  13. 0013intro hgap
  14. 0014cases hlcm
  15. 0015specialize hlcm_right k
  16. 0016apply hlcm_right
  17. 0017intro i
  18. 0018intro m
  19. 0019intro hi
  20. 0020intro hm
  21. 0021have hresidue : exists a. (((exists ff_h_gcrt_gap_decoded_residue. ff_h_gcrt_gap_decoded_residue + S (a) = S ((S (i)) * s)) /\ exists ff_q_gcrt_gap_decoded_residue. r = ff_q_gcrt_gap_decoded_residue * S ((S (i)) * s) + (a)))
  22. 0022specialize beta_at_exists r
  23. 0023specialize beta_at_exists s
  24. 0024specialize beta_at_exists i
  25. 0025exact beta_at_exists
  26. 0026cases hresidue
  27. 0027specialize mod_eq_ordered_gap_multiple m
  28. 0028specialize mod_eq_ordered_gap_multiple k
  29. 0029specialize mod_eq_ordered_gap_multiple x
  30. 0030specialize mod_eq_ordered_gap_multiple y
  31. 0031apply mod_eq_ordered_gap_multiple
  32. 0032exact hgap
  33. 0033specialize crt_prefix_solutions_pointwise_congruent r
  34. 0034specialize crt_prefix_solutions_pointwise_congruent s
  35. 0035specialize crt_prefix_solutions_pointwise_congruent b
  36. 0036specialize crt_prefix_solutions_pointwise_congruent c
  37. 0037specialize crt_prefix_solutions_pointwise_congruent l
  38. 0038specialize crt_prefix_solutions_pointwise_congruent x
  39. 0039specialize crt_prefix_solutions_pointwise_congruent y
  40. 0040specialize crt_prefix_solutions_pointwise_congruent i
  41. 0041specialize crt_prefix_solutions_pointwise_congruent x1
  42. 0042specialize crt_prefix_solutions_pointwise_congruent m
  43. 0043apply crt_prefix_solutions_pointwise_congruent
  44. 0044exact hx
  45. 0045exact hy
  46. 0046exact hi
  47. 0047exact hresidue_witness
  48. 0048exact hm