CR0018

crt_prefix_solution_class_iff_lcm

The complete solution class of any finite system is exactly one congruence class modulo its 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,y,x)) ∧ (ModEq(M,y,x) → CRTPrefixSolution(r,s,b,c,l,y))

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

Definition DAG

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

Actual proof prerequisites

crt_prefix_solutions_congruent_lcmcrt_prefix_solution_transport_common_multiple
Original expanded first-order statement 
forall r s b c l M x y. (((forall gcrt_common_index_iff_lcm_own gcrt_common_modulus_iff_lcm_own. (exists ff_lt_gcrt_iff_lcm_own_bound. ff_lt_gcrt_iff_lcm_own_bound + S gcrt_common_index_iff_lcm_own = l) -> (((exists ff_h_gcrt_iff_lcm_own_entry. ff_h_gcrt_iff_lcm_own_entry + S (gcrt_common_modulus_iff_lcm_own) = S ((S (gcrt_common_index_iff_lcm_own)) * c)) /\ exists ff_q_gcrt_iff_lcm_own_entry. b = ff_q_gcrt_iff_lcm_own_entry * S ((S (gcrt_common_index_iff_lcm_own)) * c) + (gcrt_common_modulus_iff_lcm_own))) -> exists gcrt_common_quotient_iff_lcm_own. M = gcrt_common_modulus_iff_lcm_own * gcrt_common_quotient_iff_lcm_own) /\ forall gcrt_lcm_common_iff_lcm. (forall gcrt_common_index_iff_lcm_other gcrt_common_modulus_iff_lcm_other. (exists ff_lt_gcrt_iff_lcm_other_bound. ff_lt_gcrt_iff_lcm_other_bound + S gcrt_common_index_iff_lcm_other = l) -> (((exists ff_h_gcrt_iff_lcm_other_entry. ff_h_gcrt_iff_lcm_other_entry + S (gcrt_common_modulus_iff_lcm_other) = S ((S (gcrt_common_index_iff_lcm_other)) * c)) /\ exists ff_q_gcrt_iff_lcm_other_entry. b = ff_q_gcrt_iff_lcm_other_entry * S ((S (gcrt_common_index_iff_lcm_other)) * c) + (gcrt_common_modulus_iff_lcm_other))) -> exists gcrt_common_quotient_iff_lcm_other. gcrt_lcm_common_iff_lcm = gcrt_common_modulus_iff_lcm_other * gcrt_common_quotient_iff_lcm_other) -> exists gcrt_lcm_quotient_iff_lcm. gcrt_lcm_common_iff_lcm = M * gcrt_lcm_quotient_iff_lcm)) -> (forall gcrt_solution_index_iff_fixed gcrt_solution_residue_iff_fixed gcrt_solution_modulus_iff_fixed. (exists ff_lt_gcrt_iff_fixed_bound. ff_lt_gcrt_iff_fixed_bound + S gcrt_solution_index_iff_fixed = l) -> (((exists ff_h_gcrt_iff_fixed_residue. ff_h_gcrt_iff_fixed_residue + S (gcrt_solution_residue_iff_fixed) = S ((S (gcrt_solution_index_iff_fixed)) * s)) /\ exists ff_q_gcrt_iff_fixed_residue. r = ff_q_gcrt_iff_fixed_residue * S ((S (gcrt_solution_index_iff_fixed)) * s) + (gcrt_solution_residue_iff_fixed))) -> (((exists ff_h_gcrt_iff_fixed_modulus. ff_h_gcrt_iff_fixed_modulus + S (gcrt_solution_modulus_iff_fixed) = S ((S (gcrt_solution_index_iff_fixed)) * c)) /\ exists ff_q_gcrt_iff_fixed_modulus. b = ff_q_gcrt_iff_fixed_modulus * S ((S (gcrt_solution_index_iff_fixed)) * c) + (gcrt_solution_modulus_iff_fixed))) -> (exists hgcrt_mod_left_gcrt_iff_fixed_congruence hgcrt_mod_right_gcrt_iff_fixed_congruence. x + gcrt_solution_modulus_iff_fixed * hgcrt_mod_left_gcrt_iff_fixed_congruence = gcrt_solution_residue_iff_fixed + gcrt_solution_modulus_iff_fixed * hgcrt_mod_right_gcrt_iff_fixed_congruence)) -> (((forall gcrt_solution_index_iff_candidate_forward gcrt_solution_residue_iff_candidate_forward gcrt_solution_modulus_iff_candidate_forward. (exists ff_lt_gcrt_iff_candidate_forward_bound. ff_lt_gcrt_iff_candidate_forward_bound + S gcrt_solution_index_iff_candidate_forward = l) -> (((exists ff_h_gcrt_iff_candidate_forward_residue. ff_h_gcrt_iff_candidate_forward_residue + S (gcrt_solution_residue_iff_candidate_forward) = S ((S (gcrt_solution_index_iff_candidate_forward)) * s)) /\ exists ff_q_gcrt_iff_candidate_forward_residue. r = ff_q_gcrt_iff_candidate_forward_residue * S ((S (gcrt_solution_index_iff_candidate_forward)) * s) + (gcrt_solution_residue_iff_candidate_forward))) -> (((exists ff_h_gcrt_iff_candidate_forward_modulus. ff_h_gcrt_iff_candidate_forward_modulus + S (gcrt_solution_modulus_iff_candidate_forward) = S ((S (gcrt_solution_index_iff_candidate_forward)) * c)) /\ exists ff_q_gcrt_iff_candidate_forward_modulus. b = ff_q_gcrt_iff_candidate_forward_modulus * S ((S (gcrt_solution_index_iff_candidate_forward)) * c) + (gcrt_solution_modulus_iff_candidate_forward))) -> (exists hgcrt_mod_left_gcrt_iff_candidate_forward_congruence hgcrt_mod_right_gcrt_iff_candidate_forward_congruence. y + gcrt_solution_modulus_iff_candidate_forward * hgcrt_mod_left_gcrt_iff_candidate_forward_congruence = gcrt_solution_residue_iff_candidate_forward + gcrt_solution_modulus_iff_candidate_forward * hgcrt_mod_right_gcrt_iff_candidate_forward_congruence)) -> (exists hgcrt_mod_left_gcrt_iff_mod_forward hgcrt_mod_right_gcrt_iff_mod_forward. y + M * hgcrt_mod_left_gcrt_iff_mod_forward = x + M * hgcrt_mod_right_gcrt_iff_mod_forward)) /\ ((exists hgcrt_mod_left_gcrt_iff_mod_reverse hgcrt_mod_right_gcrt_iff_mod_reverse. y + M * hgcrt_mod_left_gcrt_iff_mod_reverse = x + M * hgcrt_mod_right_gcrt_iff_mod_reverse) -> (forall gcrt_solution_index_iff_candidate_reverse gcrt_solution_residue_iff_candidate_reverse gcrt_solution_modulus_iff_candidate_reverse. (exists ff_lt_gcrt_iff_candidate_reverse_bound. ff_lt_gcrt_iff_candidate_reverse_bound + S gcrt_solution_index_iff_candidate_reverse = l) -> (((exists ff_h_gcrt_iff_candidate_reverse_residue. ff_h_gcrt_iff_candidate_reverse_residue + S (gcrt_solution_residue_iff_candidate_reverse) = S ((S (gcrt_solution_index_iff_candidate_reverse)) * s)) /\ exists ff_q_gcrt_iff_candidate_reverse_residue. r = ff_q_gcrt_iff_candidate_reverse_residue * S ((S (gcrt_solution_index_iff_candidate_reverse)) * s) + (gcrt_solution_residue_iff_candidate_reverse))) -> (((exists ff_h_gcrt_iff_candidate_reverse_modulus. ff_h_gcrt_iff_candidate_reverse_modulus + S (gcrt_solution_modulus_iff_candidate_reverse) = S ((S (gcrt_solution_index_iff_candidate_reverse)) * c)) /\ exists ff_q_gcrt_iff_candidate_reverse_modulus. b = ff_q_gcrt_iff_candidate_reverse_modulus * S ((S (gcrt_solution_index_iff_candidate_reverse)) * c) + (gcrt_solution_modulus_iff_candidate_reverse))) -> (exists hgcrt_mod_left_gcrt_iff_candidate_reverse_congruence hgcrt_mod_right_gcrt_iff_candidate_reverse_congruence. y + gcrt_solution_modulus_iff_candidate_reverse * hgcrt_mod_left_gcrt_iff_candidate_reverse_congruence = gcrt_solution_residue_iff_candidate_reverse + gcrt_solution_modulus_iff_candidate_reverse * hgcrt_mod_right_gcrt_iff_candidate_reverse_congruence))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

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

Named ingredients (2)
crt prefix solutions congruent lcmcrt prefix solution transport common 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
02Separate the logical casesL11–11

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

  1. L11
    split
03Fix variables and assumptionsL12–12

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

  1. L12
    intro hy
04Use earlier factsL13–22

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

  1. L13
    specialize crt_prefix_solutions_congruent_lcm r
  2. L14
    specialize crt_prefix_solutions_congruent_lcm s
  3. L15
    specialize crt_prefix_solutions_congruent_lcm b
  4. L16
    specialize crt_prefix_solutions_congruent_lcm c
  5. L17
    specialize crt_prefix_solutions_congruent_lcm l
  6. L18
    specialize crt_prefix_solutions_congruent_lcm M
  7. L19
    specialize crt_prefix_solutions_congruent_lcm y
  8. L20
    specialize crt_prefix_solutions_congruent_lcm x
  9. L21
    apply crt_prefix_solutions_congruent_lcm
  10. L22
    exact hlcm
05Use earlier factsL23–24

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

  1. L23
    exact hy
  2. L24
    exact hx
06Fix variables and assumptionsL25–25

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

  1. L25
    intro hmod
07Separate the logical casesL26–26

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

  1. L26
    cases hlcm
08Use earlier factsL27–36

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

  1. L27
    specialize crt_prefix_solution_transport_common_multiple r
  2. L28
    specialize crt_prefix_solution_transport_common_multiple s
  3. L29
    specialize crt_prefix_solution_transport_common_multiple b
  4. L30
    specialize crt_prefix_solution_transport_common_multiple c
  5. L31
    specialize crt_prefix_solution_transport_common_multiple l
  6. L32
    specialize crt_prefix_solution_transport_common_multiple M
  7. L33
    specialize crt_prefix_solution_transport_common_multiple x
  8. L34
    specialize crt_prefix_solution_transport_common_multiple y
  9. L35
    apply crt_prefix_solution_transport_common_multiple
  10. L36
    exact hlcm_left
09Use earlier factsL37–38

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

  1. L37
    exact hx
  2. L38
    exact hmod

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 M
  7. 0007intro x
  8. 0008intro y
  9. 0009intro hlcm
  10. 0010intro hx
  11. 0011split
  12. 0012intro hy
  13. 0013specialize crt_prefix_solutions_congruent_lcm r
  14. 0014specialize crt_prefix_solutions_congruent_lcm s
  15. 0015specialize crt_prefix_solutions_congruent_lcm b
  16. 0016specialize crt_prefix_solutions_congruent_lcm c
  17. 0017specialize crt_prefix_solutions_congruent_lcm l
  18. 0018specialize crt_prefix_solutions_congruent_lcm M
  19. 0019specialize crt_prefix_solutions_congruent_lcm y
  20. 0020specialize crt_prefix_solutions_congruent_lcm x
  21. 0021apply crt_prefix_solutions_congruent_lcm
  22. 0022exact hlcm
  23. 0023exact hy
  24. 0024exact hx
  25. 0025intro hmod
  26. 0026cases hlcm
  27. 0027specialize crt_prefix_solution_transport_common_multiple r
  28. 0028specialize crt_prefix_solution_transport_common_multiple s
  29. 0029specialize crt_prefix_solution_transport_common_multiple b
  30. 0030specialize crt_prefix_solution_transport_common_multiple c
  31. 0031specialize crt_prefix_solution_transport_common_multiple l
  32. 0032specialize crt_prefix_solution_transport_common_multiple M
  33. 0033specialize crt_prefix_solution_transport_common_multiple x
  34. 0034specialize crt_prefix_solution_transport_common_multiple y
  35. 0035apply crt_prefix_solution_transport_common_multiple
  36. 0036exact hlcm_left
  37. 0037exact hx
  38. 0038exact hmod