CR0019

crt_prefix_solution_canonical_remainder

Every existing finite-list solution has an actual canonical representative strictly below its nonzero 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. ¬M = 0 → CRTPrefixLCM(b,c,l,M) → CRTPrefixSolution(r,s,b,c,l,x) → ∃ y. CRTCanonicalPrefixSolution(r,s,b,c,l,y,M)

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

Definition DAG

CRTPrefixSolution(r,s,b,c,l,x) · 1CRTPrefixLCM(b,c,l,M) · 1CRTCanonicalPrefixSolution(r,s,b,c,l,x,M) · 1

Actual proof prerequisites

canonical_remainder_exists · checked external prerequisiteremainder_decomposition_to_mod_eq · checked external prerequisitemul_comm · checked external prerequisitemod_eq_symm · checked external prerequisitecrt_prefix_solution_transport_common_multiple
Original expanded first-order statement 
forall r s b c l M x. ~(M = 0) -> (((forall gcrt_common_index_canonical_remainder_lcm_own gcrt_common_modulus_canonical_remainder_lcm_own. (exists ff_lt_gcrt_canonical_remainder_lcm_own_bound. ff_lt_gcrt_canonical_remainder_lcm_own_bound + S gcrt_common_index_canonical_remainder_lcm_own = l) -> (((exists ff_h_gcrt_canonical_remainder_lcm_own_entry. ff_h_gcrt_canonical_remainder_lcm_own_entry + S (gcrt_common_modulus_canonical_remainder_lcm_own) = S ((S (gcrt_common_index_canonical_remainder_lcm_own)) * c)) /\ exists ff_q_gcrt_canonical_remainder_lcm_own_entry. b = ff_q_gcrt_canonical_remainder_lcm_own_entry * S ((S (gcrt_common_index_canonical_remainder_lcm_own)) * c) + (gcrt_common_modulus_canonical_remainder_lcm_own))) -> exists gcrt_common_quotient_canonical_remainder_lcm_own. M = gcrt_common_modulus_canonical_remainder_lcm_own * gcrt_common_quotient_canonical_remainder_lcm_own) /\ forall gcrt_lcm_common_canonical_remainder_lcm. (forall gcrt_common_index_canonical_remainder_lcm_other gcrt_common_modulus_canonical_remainder_lcm_other. (exists ff_lt_gcrt_canonical_remainder_lcm_other_bound. ff_lt_gcrt_canonical_remainder_lcm_other_bound + S gcrt_common_index_canonical_remainder_lcm_other = l) -> (((exists ff_h_gcrt_canonical_remainder_lcm_other_entry. ff_h_gcrt_canonical_remainder_lcm_other_entry + S (gcrt_common_modulus_canonical_remainder_lcm_other) = S ((S (gcrt_common_index_canonical_remainder_lcm_other)) * c)) /\ exists ff_q_gcrt_canonical_remainder_lcm_other_entry. b = ff_q_gcrt_canonical_remainder_lcm_other_entry * S ((S (gcrt_common_index_canonical_remainder_lcm_other)) * c) + (gcrt_common_modulus_canonical_remainder_lcm_other))) -> exists gcrt_common_quotient_canonical_remainder_lcm_other. gcrt_lcm_common_canonical_remainder_lcm = gcrt_common_modulus_canonical_remainder_lcm_other * gcrt_common_quotient_canonical_remainder_lcm_other) -> exists gcrt_lcm_quotient_canonical_remainder_lcm. gcrt_lcm_common_canonical_remainder_lcm = M * gcrt_lcm_quotient_canonical_remainder_lcm)) -> (forall gcrt_solution_index_canonical_remainder_source gcrt_solution_residue_canonical_remainder_source gcrt_solution_modulus_canonical_remainder_source. (exists ff_lt_gcrt_canonical_remainder_source_bound. ff_lt_gcrt_canonical_remainder_source_bound + S gcrt_solution_index_canonical_remainder_source = l) -> (((exists ff_h_gcrt_canonical_remainder_source_residue. ff_h_gcrt_canonical_remainder_source_residue + S (gcrt_solution_residue_canonical_remainder_source) = S ((S (gcrt_solution_index_canonical_remainder_source)) * s)) /\ exists ff_q_gcrt_canonical_remainder_source_residue. r = ff_q_gcrt_canonical_remainder_source_residue * S ((S (gcrt_solution_index_canonical_remainder_source)) * s) + (gcrt_solution_residue_canonical_remainder_source))) -> (((exists ff_h_gcrt_canonical_remainder_source_modulus. ff_h_gcrt_canonical_remainder_source_modulus + S (gcrt_solution_modulus_canonical_remainder_source) = S ((S (gcrt_solution_index_canonical_remainder_source)) * c)) /\ exists ff_q_gcrt_canonical_remainder_source_modulus. b = ff_q_gcrt_canonical_remainder_source_modulus * S ((S (gcrt_solution_index_canonical_remainder_source)) * c) + (gcrt_solution_modulus_canonical_remainder_source))) -> (exists hgcrt_mod_left_gcrt_canonical_remainder_source_congruence hgcrt_mod_right_gcrt_canonical_remainder_source_congruence. x + gcrt_solution_modulus_canonical_remainder_source * hgcrt_mod_left_gcrt_canonical_remainder_source_congruence = gcrt_solution_residue_canonical_remainder_source + gcrt_solution_modulus_canonical_remainder_source * hgcrt_mod_right_gcrt_canonical_remainder_source_congruence)) -> exists y. (((((forall gcrt_common_index_canonical_remainder_result_lcm_own gcrt_common_modulus_canonical_remainder_result_lcm_own. (exists ff_lt_gcrt_canonical_remainder_result_lcm_own_bound. ff_lt_gcrt_canonical_remainder_result_lcm_own_bound + S gcrt_common_index_canonical_remainder_result_lcm_own = l) -> (((exists ff_h_gcrt_canonical_remainder_result_lcm_own_entry. ff_h_gcrt_canonical_remainder_result_lcm_own_entry + S (gcrt_common_modulus_canonical_remainder_result_lcm_own) = S ((S (gcrt_common_index_canonical_remainder_result_lcm_own)) * c)) /\ exists ff_q_gcrt_canonical_remainder_result_lcm_own_entry. b = ff_q_gcrt_canonical_remainder_result_lcm_own_entry * S ((S (gcrt_common_index_canonical_remainder_result_lcm_own)) * c) + (gcrt_common_modulus_canonical_remainder_result_lcm_own))) -> exists gcrt_common_quotient_canonical_remainder_result_lcm_own. M = gcrt_common_modulus_canonical_remainder_result_lcm_own * gcrt_common_quotient_canonical_remainder_result_lcm_own) /\ forall gcrt_lcm_common_canonical_remainder_result_lcm. (forall gcrt_common_index_canonical_remainder_result_lcm_other gcrt_common_modulus_canonical_remainder_result_lcm_other. (exists ff_lt_gcrt_canonical_remainder_result_lcm_other_bound. ff_lt_gcrt_canonical_remainder_result_lcm_other_bound + S gcrt_common_index_canonical_remainder_result_lcm_other = l) -> (((exists ff_h_gcrt_canonical_remainder_result_lcm_other_entry. ff_h_gcrt_canonical_remainder_result_lcm_other_entry + S (gcrt_common_modulus_canonical_remainder_result_lcm_other) = S ((S (gcrt_common_index_canonical_remainder_result_lcm_other)) * c)) /\ exists ff_q_gcrt_canonical_remainder_result_lcm_other_entry. b = ff_q_gcrt_canonical_remainder_result_lcm_other_entry * S ((S (gcrt_common_index_canonical_remainder_result_lcm_other)) * c) + (gcrt_common_modulus_canonical_remainder_result_lcm_other))) -> exists gcrt_common_quotient_canonical_remainder_result_lcm_other. gcrt_lcm_common_canonical_remainder_result_lcm = gcrt_common_modulus_canonical_remainder_result_lcm_other * gcrt_common_quotient_canonical_remainder_result_lcm_other) -> exists gcrt_lcm_quotient_canonical_remainder_result_lcm. gcrt_lcm_common_canonical_remainder_result_lcm = M * gcrt_lcm_quotient_canonical_remainder_result_lcm)) /\ ((exists ff_lt_gcrt_canonical_remainder_result_bounded. ff_lt_gcrt_canonical_remainder_result_bounded + S y = M) /\ (forall gcrt_solution_index_canonical_remainder_result_solution gcrt_solution_residue_canonical_remainder_result_solution gcrt_solution_modulus_canonical_remainder_result_solution. (exists ff_lt_gcrt_canonical_remainder_result_solution_bound. ff_lt_gcrt_canonical_remainder_result_solution_bound + S gcrt_solution_index_canonical_remainder_result_solution = l) -> (((exists ff_h_gcrt_canonical_remainder_result_solution_residue. ff_h_gcrt_canonical_remainder_result_solution_residue + S (gcrt_solution_residue_canonical_remainder_result_solution) = S ((S (gcrt_solution_index_canonical_remainder_result_solution)) * s)) /\ exists ff_q_gcrt_canonical_remainder_result_solution_residue. r = ff_q_gcrt_canonical_remainder_result_solution_residue * S ((S (gcrt_solution_index_canonical_remainder_result_solution)) * s) + (gcrt_solution_residue_canonical_remainder_result_solution))) -> (((exists ff_h_gcrt_canonical_remainder_result_solution_modulus. ff_h_gcrt_canonical_remainder_result_solution_modulus + S (gcrt_solution_modulus_canonical_remainder_result_solution) = S ((S (gcrt_solution_index_canonical_remainder_result_solution)) * c)) /\ exists ff_q_gcrt_canonical_remainder_result_solution_modulus. b = ff_q_gcrt_canonical_remainder_result_solution_modulus * S ((S (gcrt_solution_index_canonical_remainder_result_solution)) * c) + (gcrt_solution_modulus_canonical_remainder_result_solution))) -> (exists hgcrt_mod_left_gcrt_canonical_remainder_result_solution_congruence hgcrt_mod_right_gcrt_canonical_remainder_result_solution_congruence. y + gcrt_solution_modulus_canonical_remainder_result_solution * hgcrt_mod_left_gcrt_canonical_remainder_result_solution_congruence = gcrt_solution_residue_canonical_remainder_result_solution + gcrt_solution_modulus_canonical_remainder_result_solution * hgcrt_mod_right_gcrt_canonical_remainder_result_solution_congruence)))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

53 script commands · 14 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 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 hnonzero
  9. L9
    intro hlcm
  10. L10
    intro hx
02Establish hremL11–15

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

  1. L11
    have hrem : exists y. ((exists q. x = M * q + y) /\ exists gap. gap + S y = M)
  2. L12
    specialize canonical_remainder_exists M
  3. L13
    specialize canonical_remainder_exists x
  4. L14
    apply canonical_remainder_exists
  5. L15
    exact hnonzero
03Separate the logical casesL16–18

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

  1. L16
    cases hrem
  2. L17
    cases hrem_witness
  3. L18
    cases hrem_witness_left
04Establish hforwardL19–28

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

  1. L19
    have hforward : exists hgcrt_mod_left_gcrt_canonical_forward hgcrt_mod_right_gcrt_canonical_forward. x + M * hgcrt_mod_left_gcrt_canonical_forward = x1 + M * hgcrt_mod_right_gcrt_canonical_forward
  2. L20
    specialize remainder_decomposition_to_mod_eq M
  3. L21
    specialize remainder_decomposition_to_mod_eq x
  4. L22
    specialize remainder_decomposition_to_mod_eq x2
  5. L23
    specialize remainder_decomposition_to_mod_eq x1
  6. L24
    apply remainder_decomposition_to_mod_eq
  7. L25
    trans M * x2 + x1
  8. L26
    exact hrem_witness_left_witness
  9. L27
    congr
  10. L28
    apply mul_comm
05Calculate and transport equalitiesL29–29

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

  1. L29
    refl
06Establish hreverseL30–35

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

  1. L30
    have hreverse : exists hgcrt_mod_left_gcrt_canonical_reverse hgcrt_mod_right_gcrt_canonical_reverse. x1 + M * hgcrt_mod_left_gcrt_canonical_reverse = x + M * hgcrt_mod_right_gcrt_canonical_reverse
  2. L31
    specialize mod_eq_symm M
  3. L32
    specialize mod_eq_symm x
  4. L33
    specialize mod_eq_symm x1
  5. L34
    apply mod_eq_symm
  6. L35
    exact hforward
07Construct an explicit witnessL36–36

Supply the displayed value, then prove that it has the required property.

  1. L36
    exists x1
08Separate the logical casesL37–37

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

  1. L37
    split
09Use earlier factsL38–38

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

  1. L38
    exact hlcm
10Separate the logical casesL39–39

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

  1. L39
    split
11Use earlier factsL40–40

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

  1. L40
    exact hrem_witness_right
12Separate the logical casesL41–41

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

  1. L41
    cases hlcm
13Use earlier factsL42–51

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

  1. L42
    specialize crt_prefix_solution_transport_common_multiple r
  2. L43
    specialize crt_prefix_solution_transport_common_multiple s
  3. L44
    specialize crt_prefix_solution_transport_common_multiple b
  4. L45
    specialize crt_prefix_solution_transport_common_multiple c
  5. L46
    specialize crt_prefix_solution_transport_common_multiple l
  6. L47
    specialize crt_prefix_solution_transport_common_multiple M
  7. L48
    specialize crt_prefix_solution_transport_common_multiple x
  8. L49
    specialize crt_prefix_solution_transport_common_multiple x1
  9. L50
    apply crt_prefix_solution_transport_common_multiple
  10. L51
    exact hlcm_left
14Use earlier factsL52–53

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

  1. L52
    exact hx
  2. L53
    exact hreverse

Library-wide reading audit

Original defined command ledger · 53 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro M
  7. 0007intro x
  8. 0008intro hnonzero
  9. 0009intro hlcm
  10. 0010intro hx
  11. 0011have hrem : exists y. ((exists q. x = M * q + y) /\ exists gap. gap + S y = M)
  12. 0012specialize canonical_remainder_exists M
  13. 0013specialize canonical_remainder_exists x
  14. 0014apply canonical_remainder_exists
  15. 0015exact hnonzero
  16. 0016cases hrem
  17. 0017cases hrem_witness
  18. 0018cases hrem_witness_left
  19. 0019have hforward : exists hgcrt_mod_left_gcrt_canonical_forward hgcrt_mod_right_gcrt_canonical_forward. x + M * hgcrt_mod_left_gcrt_canonical_forward = x1 + M * hgcrt_mod_right_gcrt_canonical_forward
  20. 0020specialize remainder_decomposition_to_mod_eq M
  21. 0021specialize remainder_decomposition_to_mod_eq x
  22. 0022specialize remainder_decomposition_to_mod_eq x2
  23. 0023specialize remainder_decomposition_to_mod_eq x1
  24. 0024apply remainder_decomposition_to_mod_eq
  25. 0025trans M * x2 + x1
  26. 0026exact hrem_witness_left_witness
  27. 0027congr
  28. 0028apply mul_comm
  29. 0029refl
  30. 0030have hreverse : exists hgcrt_mod_left_gcrt_canonical_reverse hgcrt_mod_right_gcrt_canonical_reverse. x1 + M * hgcrt_mod_left_gcrt_canonical_reverse = x + M * hgcrt_mod_right_gcrt_canonical_reverse
  31. 0031specialize mod_eq_symm M
  32. 0032specialize mod_eq_symm x
  33. 0033specialize mod_eq_symm x1
  34. 0034apply mod_eq_symm
  35. 0035exact hforward
  36. 0036exists x1
  37. 0037split
  38. 0038exact hlcm
  39. 0039split
  40. 0040exact hrem_witness_right
  41. 0041cases hlcm
  42. 0042specialize crt_prefix_solution_transport_common_multiple r
  43. 0043specialize crt_prefix_solution_transport_common_multiple s
  44. 0044specialize crt_prefix_solution_transport_common_multiple b
  45. 0045specialize crt_prefix_solution_transport_common_multiple c
  46. 0046specialize crt_prefix_solution_transport_common_multiple l
  47. 0047specialize crt_prefix_solution_transport_common_multiple M
  48. 0048specialize crt_prefix_solution_transport_common_multiple x
  49. 0049specialize crt_prefix_solution_transport_common_multiple x1
  50. 0050apply crt_prefix_solution_transport_common_multiple
  51. 0051exact hlcm_left
  52. 0052exact hx
  53. 0053exact hreverse