CR0014

crt_prefix_solutions_pointwise_congruent

Two simultaneous solutions are congruent modulo every actually decoded list modulus.

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. ∀ x. ∀ y. ∀ i. ∀ a. ∀ m. CRTPrefixSolution(r,s,b,c,l,x) → CRTPrefixSolution(r,s,b,c,l,y) → Lt(i,l) → Beta(r,s,i,a) → Beta(b,c,i,m) → ModEq(m,x,y)

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

Definition DAG

Beta(b,c,i,x) · 2CRTPrefixSolution(r,s,b,c,l,x) · 2Lt(a,b) · 1ModEq(m,a,b) · 1

Actual proof prerequisites

mod_eq_symm · checked external prerequisitemod_eq_trans · checked external prerequisite
Original expanded first-order statement 
forall r s b c l x y i a m. (forall gcrt_solution_index_pointwise_solution_left gcrt_solution_residue_pointwise_solution_left gcrt_solution_modulus_pointwise_solution_left. (exists ff_lt_gcrt_pointwise_solution_left_bound. ff_lt_gcrt_pointwise_solution_left_bound + S gcrt_solution_index_pointwise_solution_left = l) -> (((exists ff_h_gcrt_pointwise_solution_left_residue. ff_h_gcrt_pointwise_solution_left_residue + S (gcrt_solution_residue_pointwise_solution_left) = S ((S (gcrt_solution_index_pointwise_solution_left)) * s)) /\ exists ff_q_gcrt_pointwise_solution_left_residue. r = ff_q_gcrt_pointwise_solution_left_residue * S ((S (gcrt_solution_index_pointwise_solution_left)) * s) + (gcrt_solution_residue_pointwise_solution_left))) -> (((exists ff_h_gcrt_pointwise_solution_left_modulus. ff_h_gcrt_pointwise_solution_left_modulus + S (gcrt_solution_modulus_pointwise_solution_left) = S ((S (gcrt_solution_index_pointwise_solution_left)) * c)) /\ exists ff_q_gcrt_pointwise_solution_left_modulus. b = ff_q_gcrt_pointwise_solution_left_modulus * S ((S (gcrt_solution_index_pointwise_solution_left)) * c) + (gcrt_solution_modulus_pointwise_solution_left))) -> (exists hgcrt_mod_left_gcrt_pointwise_solution_left_congruence hgcrt_mod_right_gcrt_pointwise_solution_left_congruence. x + gcrt_solution_modulus_pointwise_solution_left * hgcrt_mod_left_gcrt_pointwise_solution_left_congruence = gcrt_solution_residue_pointwise_solution_left + gcrt_solution_modulus_pointwise_solution_left * hgcrt_mod_right_gcrt_pointwise_solution_left_congruence)) -> (forall gcrt_solution_index_pointwise_solution_right gcrt_solution_residue_pointwise_solution_right gcrt_solution_modulus_pointwise_solution_right. (exists ff_lt_gcrt_pointwise_solution_right_bound. ff_lt_gcrt_pointwise_solution_right_bound + S gcrt_solution_index_pointwise_solution_right = l) -> (((exists ff_h_gcrt_pointwise_solution_right_residue. ff_h_gcrt_pointwise_solution_right_residue + S (gcrt_solution_residue_pointwise_solution_right) = S ((S (gcrt_solution_index_pointwise_solution_right)) * s)) /\ exists ff_q_gcrt_pointwise_solution_right_residue. r = ff_q_gcrt_pointwise_solution_right_residue * S ((S (gcrt_solution_index_pointwise_solution_right)) * s) + (gcrt_solution_residue_pointwise_solution_right))) -> (((exists ff_h_gcrt_pointwise_solution_right_modulus. ff_h_gcrt_pointwise_solution_right_modulus + S (gcrt_solution_modulus_pointwise_solution_right) = S ((S (gcrt_solution_index_pointwise_solution_right)) * c)) /\ exists ff_q_gcrt_pointwise_solution_right_modulus. b = ff_q_gcrt_pointwise_solution_right_modulus * S ((S (gcrt_solution_index_pointwise_solution_right)) * c) + (gcrt_solution_modulus_pointwise_solution_right))) -> (exists hgcrt_mod_left_gcrt_pointwise_solution_right_congruence hgcrt_mod_right_gcrt_pointwise_solution_right_congruence. y + gcrt_solution_modulus_pointwise_solution_right * hgcrt_mod_left_gcrt_pointwise_solution_right_congruence = gcrt_solution_residue_pointwise_solution_right + gcrt_solution_modulus_pointwise_solution_right * hgcrt_mod_right_gcrt_pointwise_solution_right_congruence)) -> (exists ff_lt_gcrt_pointwise_index. ff_lt_gcrt_pointwise_index + S i = l) -> (((exists ff_h_gcrt_pointwise_residue. ff_h_gcrt_pointwise_residue + S (a) = S ((S (i)) * s)) /\ exists ff_q_gcrt_pointwise_residue. r = ff_q_gcrt_pointwise_residue * S ((S (i)) * s) + (a))) -> (((exists ff_h_gcrt_pointwise_modulus. ff_h_gcrt_pointwise_modulus + S (m) = S ((S (i)) * c)) /\ exists ff_q_gcrt_pointwise_modulus. b = ff_q_gcrt_pointwise_modulus * S ((S (i)) * c) + (m))) -> (exists hgcrt_mod_left_gcrt_pointwise_result hgcrt_mod_right_gcrt_pointwise_result. x + m * hgcrt_mod_left_gcrt_pointwise_result = y + m * hgcrt_mod_right_gcrt_pointwise_result)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

38 script commands · 5 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.

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

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

  1. L11
    intro hx
  2. L12
    intro hy
  3. L13
    intro hi
  4. L14
    intro ha
  5. L15
    intro hm
03Use earlier factsL16–25

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

  1. L16
    specialize mod_eq_trans m
  2. L17
    specialize mod_eq_trans x
  3. L18
    specialize mod_eq_trans a
  4. L19
    specialize mod_eq_trans y
  5. L20
    apply mod_eq_trans
  6. L21
    specialize hx i
  7. L22
    specialize hx a
  8. L23
    specialize hx m
  9. L24
    apply hx
  10. L25
    exact hi
04Use earlier factsL26–35

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

  1. L26
    exact ha
  2. L27
    exact hm
  3. L28
    specialize mod_eq_symm m
  4. L29
    specialize mod_eq_symm y
  5. L30
    specialize mod_eq_symm a
  6. L31
    apply mod_eq_symm
  7. L32
    specialize hy i
  8. L33
    specialize hy a
  9. L34
    specialize hy m
  10. L35
    apply hy
05Use earlier factsL36–38

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

  1. L36
    exact hi
  2. L37
    exact ha
  3. L38
    exact hm

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro x
  7. 0007intro y
  8. 0008intro i
  9. 0009intro a
  10. 0010intro m
  11. 0011intro hx
  12. 0012intro hy
  13. 0013intro hi
  14. 0014intro ha
  15. 0015intro hm
  16. 0016specialize mod_eq_trans m
  17. 0017specialize mod_eq_trans x
  18. 0018specialize mod_eq_trans a
  19. 0019specialize mod_eq_trans y
  20. 0020apply mod_eq_trans
  21. 0021specialize hx i
  22. 0022specialize hx a
  23. 0023specialize hx m
  24. 0024apply hx
  25. 0025exact hi
  26. 0026exact ha
  27. 0027exact hm
  28. 0028specialize mod_eq_symm m
  29. 0029specialize mod_eq_symm y
  30. 0030specialize mod_eq_symm a
  31. 0031apply mod_eq_symm
  32. 0032specialize hy i
  33. 0033specialize hy a
  34. 0034specialize hy m
  35. 0035apply hy
  36. 0036exact hi
  37. 0037exact ha
  38. 0038exact hm