CR001A

crt_canonical_prefix_solution_unique

The strictly bounded canonical representative of any finite decoded CRT system is unique.

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. CRTCanonicalPrefixSolution(r,s,b,c,l,x,M) → CRTCanonicalPrefixSolution(r,s,b,c,l,y,M) → y = x

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

Definition DAG

CRTCanonicalPrefixSolution(r,s,b,c,l,x,M) · 2

Actual proof prerequisites

crt_prefix_solutions_congruent_lcmmod_eq_bounded_unique · checked external prerequisite
Original expanded first-order statement 
forall r s b c l M x y. (((((forall gcrt_common_index_canonical_unique_left_lcm_own gcrt_common_modulus_canonical_unique_left_lcm_own. (exists ff_lt_gcrt_canonical_unique_left_lcm_own_bound. ff_lt_gcrt_canonical_unique_left_lcm_own_bound + S gcrt_common_index_canonical_unique_left_lcm_own = l) -> (((exists ff_h_gcrt_canonical_unique_left_lcm_own_entry. ff_h_gcrt_canonical_unique_left_lcm_own_entry + S (gcrt_common_modulus_canonical_unique_left_lcm_own) = S ((S (gcrt_common_index_canonical_unique_left_lcm_own)) * c)) /\ exists ff_q_gcrt_canonical_unique_left_lcm_own_entry. b = ff_q_gcrt_canonical_unique_left_lcm_own_entry * S ((S (gcrt_common_index_canonical_unique_left_lcm_own)) * c) + (gcrt_common_modulus_canonical_unique_left_lcm_own))) -> exists gcrt_common_quotient_canonical_unique_left_lcm_own. M = gcrt_common_modulus_canonical_unique_left_lcm_own * gcrt_common_quotient_canonical_unique_left_lcm_own) /\ forall gcrt_lcm_common_canonical_unique_left_lcm. (forall gcrt_common_index_canonical_unique_left_lcm_other gcrt_common_modulus_canonical_unique_left_lcm_other. (exists ff_lt_gcrt_canonical_unique_left_lcm_other_bound. ff_lt_gcrt_canonical_unique_left_lcm_other_bound + S gcrt_common_index_canonical_unique_left_lcm_other = l) -> (((exists ff_h_gcrt_canonical_unique_left_lcm_other_entry. ff_h_gcrt_canonical_unique_left_lcm_other_entry + S (gcrt_common_modulus_canonical_unique_left_lcm_other) = S ((S (gcrt_common_index_canonical_unique_left_lcm_other)) * c)) /\ exists ff_q_gcrt_canonical_unique_left_lcm_other_entry. b = ff_q_gcrt_canonical_unique_left_lcm_other_entry * S ((S (gcrt_common_index_canonical_unique_left_lcm_other)) * c) + (gcrt_common_modulus_canonical_unique_left_lcm_other))) -> exists gcrt_common_quotient_canonical_unique_left_lcm_other. gcrt_lcm_common_canonical_unique_left_lcm = gcrt_common_modulus_canonical_unique_left_lcm_other * gcrt_common_quotient_canonical_unique_left_lcm_other) -> exists gcrt_lcm_quotient_canonical_unique_left_lcm. gcrt_lcm_common_canonical_unique_left_lcm = M * gcrt_lcm_quotient_canonical_unique_left_lcm)) /\ ((exists ff_lt_gcrt_canonical_unique_left_bounded. ff_lt_gcrt_canonical_unique_left_bounded + S x = M) /\ (forall gcrt_solution_index_canonical_unique_left_solution gcrt_solution_residue_canonical_unique_left_solution gcrt_solution_modulus_canonical_unique_left_solution. (exists ff_lt_gcrt_canonical_unique_left_solution_bound. ff_lt_gcrt_canonical_unique_left_solution_bound + S gcrt_solution_index_canonical_unique_left_solution = l) -> (((exists ff_h_gcrt_canonical_unique_left_solution_residue. ff_h_gcrt_canonical_unique_left_solution_residue + S (gcrt_solution_residue_canonical_unique_left_solution) = S ((S (gcrt_solution_index_canonical_unique_left_solution)) * s)) /\ exists ff_q_gcrt_canonical_unique_left_solution_residue. r = ff_q_gcrt_canonical_unique_left_solution_residue * S ((S (gcrt_solution_index_canonical_unique_left_solution)) * s) + (gcrt_solution_residue_canonical_unique_left_solution))) -> (((exists ff_h_gcrt_canonical_unique_left_solution_modulus. ff_h_gcrt_canonical_unique_left_solution_modulus + S (gcrt_solution_modulus_canonical_unique_left_solution) = S ((S (gcrt_solution_index_canonical_unique_left_solution)) * c)) /\ exists ff_q_gcrt_canonical_unique_left_solution_modulus. b = ff_q_gcrt_canonical_unique_left_solution_modulus * S ((S (gcrt_solution_index_canonical_unique_left_solution)) * c) + (gcrt_solution_modulus_canonical_unique_left_solution))) -> (exists hgcrt_mod_left_gcrt_canonical_unique_left_solution_congruence hgcrt_mod_right_gcrt_canonical_unique_left_solution_congruence. x + gcrt_solution_modulus_canonical_unique_left_solution * hgcrt_mod_left_gcrt_canonical_unique_left_solution_congruence = gcrt_solution_residue_canonical_unique_left_solution + gcrt_solution_modulus_canonical_unique_left_solution * hgcrt_mod_right_gcrt_canonical_unique_left_solution_congruence))))) -> (((((forall gcrt_common_index_canonical_unique_right_lcm_own gcrt_common_modulus_canonical_unique_right_lcm_own. (exists ff_lt_gcrt_canonical_unique_right_lcm_own_bound. ff_lt_gcrt_canonical_unique_right_lcm_own_bound + S gcrt_common_index_canonical_unique_right_lcm_own = l) -> (((exists ff_h_gcrt_canonical_unique_right_lcm_own_entry. ff_h_gcrt_canonical_unique_right_lcm_own_entry + S (gcrt_common_modulus_canonical_unique_right_lcm_own) = S ((S (gcrt_common_index_canonical_unique_right_lcm_own)) * c)) /\ exists ff_q_gcrt_canonical_unique_right_lcm_own_entry. b = ff_q_gcrt_canonical_unique_right_lcm_own_entry * S ((S (gcrt_common_index_canonical_unique_right_lcm_own)) * c) + (gcrt_common_modulus_canonical_unique_right_lcm_own))) -> exists gcrt_common_quotient_canonical_unique_right_lcm_own. M = gcrt_common_modulus_canonical_unique_right_lcm_own * gcrt_common_quotient_canonical_unique_right_lcm_own) /\ forall gcrt_lcm_common_canonical_unique_right_lcm. (forall gcrt_common_index_canonical_unique_right_lcm_other gcrt_common_modulus_canonical_unique_right_lcm_other. (exists ff_lt_gcrt_canonical_unique_right_lcm_other_bound. ff_lt_gcrt_canonical_unique_right_lcm_other_bound + S gcrt_common_index_canonical_unique_right_lcm_other = l) -> (((exists ff_h_gcrt_canonical_unique_right_lcm_other_entry. ff_h_gcrt_canonical_unique_right_lcm_other_entry + S (gcrt_common_modulus_canonical_unique_right_lcm_other) = S ((S (gcrt_common_index_canonical_unique_right_lcm_other)) * c)) /\ exists ff_q_gcrt_canonical_unique_right_lcm_other_entry. b = ff_q_gcrt_canonical_unique_right_lcm_other_entry * S ((S (gcrt_common_index_canonical_unique_right_lcm_other)) * c) + (gcrt_common_modulus_canonical_unique_right_lcm_other))) -> exists gcrt_common_quotient_canonical_unique_right_lcm_other. gcrt_lcm_common_canonical_unique_right_lcm = gcrt_common_modulus_canonical_unique_right_lcm_other * gcrt_common_quotient_canonical_unique_right_lcm_other) -> exists gcrt_lcm_quotient_canonical_unique_right_lcm. gcrt_lcm_common_canonical_unique_right_lcm = M * gcrt_lcm_quotient_canonical_unique_right_lcm)) /\ ((exists ff_lt_gcrt_canonical_unique_right_bounded. ff_lt_gcrt_canonical_unique_right_bounded + S y = M) /\ (forall gcrt_solution_index_canonical_unique_right_solution gcrt_solution_residue_canonical_unique_right_solution gcrt_solution_modulus_canonical_unique_right_solution. (exists ff_lt_gcrt_canonical_unique_right_solution_bound. ff_lt_gcrt_canonical_unique_right_solution_bound + S gcrt_solution_index_canonical_unique_right_solution = l) -> (((exists ff_h_gcrt_canonical_unique_right_solution_residue. ff_h_gcrt_canonical_unique_right_solution_residue + S (gcrt_solution_residue_canonical_unique_right_solution) = S ((S (gcrt_solution_index_canonical_unique_right_solution)) * s)) /\ exists ff_q_gcrt_canonical_unique_right_solution_residue. r = ff_q_gcrt_canonical_unique_right_solution_residue * S ((S (gcrt_solution_index_canonical_unique_right_solution)) * s) + (gcrt_solution_residue_canonical_unique_right_solution))) -> (((exists ff_h_gcrt_canonical_unique_right_solution_modulus. ff_h_gcrt_canonical_unique_right_solution_modulus + S (gcrt_solution_modulus_canonical_unique_right_solution) = S ((S (gcrt_solution_index_canonical_unique_right_solution)) * c)) /\ exists ff_q_gcrt_canonical_unique_right_solution_modulus. b = ff_q_gcrt_canonical_unique_right_solution_modulus * S ((S (gcrt_solution_index_canonical_unique_right_solution)) * c) + (gcrt_solution_modulus_canonical_unique_right_solution))) -> (exists hgcrt_mod_left_gcrt_canonical_unique_right_solution_congruence hgcrt_mod_right_gcrt_canonical_unique_right_solution_congruence. y + gcrt_solution_modulus_canonical_unique_right_solution * hgcrt_mod_left_gcrt_canonical_unique_right_solution_congruence = gcrt_solution_residue_canonical_unique_right_solution + gcrt_solution_modulus_canonical_unique_right_solution * hgcrt_mod_right_gcrt_canonical_unique_right_solution_congruence))))) -> y = x

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

32 script commands · 4 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 (1)
crt prefix solutions congruent lcm
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 hx
  10. L10
    intro hy
02Separate the logical casesL11–14

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

  1. L11
    cases hx
  2. L12
    cases hx_right
  3. L13
    cases hy
  4. L14
    cases hy_right
03Use earlier factsL15–24

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

  1. L15
    specialize mod_eq_bounded_unique M
  2. L16
    specialize mod_eq_bounded_unique y
  3. L17
    specialize mod_eq_bounded_unique x
  4. L18
    apply mod_eq_bounded_unique
  5. L19
    exact hy_right_left
  6. L20
    exact hx_right_left
  7. L21
    specialize crt_prefix_solutions_congruent_lcm r
  8. L22
    specialize crt_prefix_solutions_congruent_lcm s
  9. L23
    specialize crt_prefix_solutions_congruent_lcm b
  10. L24
    specialize crt_prefix_solutions_congruent_lcm c
04Use earlier factsL25–32

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

  1. L25
    specialize crt_prefix_solutions_congruent_lcm l
  2. L26
    specialize crt_prefix_solutions_congruent_lcm M
  3. L27
    specialize crt_prefix_solutions_congruent_lcm y
  4. L28
    specialize crt_prefix_solutions_congruent_lcm x
  5. L29
    apply crt_prefix_solutions_congruent_lcm
  6. L30
    exact hx_left
  7. L31
    exact hy_right_right
  8. L32
    exact hx_right_right

Library-wide reading audit

Original defined command ledger · 32 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 hx
  10. 0010intro hy
  11. 0011cases hx
  12. 0012cases hx_right
  13. 0013cases hy
  14. 0014cases hy_right
  15. 0015specialize mod_eq_bounded_unique M
  16. 0016specialize mod_eq_bounded_unique y
  17. 0017specialize mod_eq_bounded_unique x
  18. 0018apply mod_eq_bounded_unique
  19. 0019exact hy_right_left
  20. 0020exact hx_right_left
  21. 0021specialize crt_prefix_solutions_congruent_lcm r
  22. 0022specialize crt_prefix_solutions_congruent_lcm s
  23. 0023specialize crt_prefix_solutions_congruent_lcm b
  24. 0024specialize crt_prefix_solutions_congruent_lcm c
  25. 0025specialize crt_prefix_solutions_congruent_lcm l
  26. 0026specialize crt_prefix_solutions_congruent_lcm M
  27. 0027specialize crt_prefix_solutions_congruent_lcm y
  28. 0028specialize crt_prefix_solutions_congruent_lcm x
  29. 0029apply crt_prefix_solutions_congruent_lcm
  30. 0030exact hx_left
  31. 0031exact hy_right_right
  32. 0032exact hx_right_right