CR001A

crt_canonical_prefix_solution_unique

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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.

Exact expanded first-order arithmetic 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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 32 exact native proof lines.

Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

CR0017 crt_prefix_solutions_congruent_lcm mod_eq_bounded_unique Stable theorem; checked-use authorized

Direct dependents

CR001B crt_pairwise_coprime_prefix_canonical_exists_unique

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 exact 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

Separate complete second-wave branches: Full G011 proof · Alpha v27.