FC0011

crt_normalized_prefix_solution_unique

Normalized representatives are literally unique at every list LCM; the zero case uses congruence equality, not a false bound below zero.

Alpha v34 checked-use · first admitted v27 · 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.

All finite lists are included, even the empty list and zero moduli. A positive LCM gives x<M; at zero LCM congruence is exact equality and normalization deliberately does not require the impossible x<0.

Exact theorem in conservative defined notation

∀ r. ∀ s. ∀ b. ∀ c. ∀ l. ∀ M. ∀ x. ∀ y. CRTNormalizedPrefixSolution(r,s,b,c,l,x,M) → CRTNormalizedPrefixSolution(r,s,b,c,l,y,M) → y = x

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

Definition DAG

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

Actual proof prerequisites

crt_prefix_zero_lcm_solution_unique · checked external prerequisitecrt_canonical_prefix_solution_unique · checked external prerequisite
Original expanded first-order statement 
forall r s b c l M x y. (((((forall gcrt_common_index_gfull_normalized_unique_left_lcm_own gcrt_common_modulus_gfull_normalized_unique_left_lcm_own. (exists ff_lt_gcrt_gfull_normalized_unique_left_lcm_own_bound. ff_lt_gcrt_gfull_normalized_unique_left_lcm_own_bound + S gcrt_common_index_gfull_normalized_unique_left_lcm_own = l) -> (((exists ff_h_gcrt_gfull_normalized_unique_left_lcm_own_entry. ff_h_gcrt_gfull_normalized_unique_left_lcm_own_entry + S (gcrt_common_modulus_gfull_normalized_unique_left_lcm_own) = S ((S (gcrt_common_index_gfull_normalized_unique_left_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_normalized_unique_left_lcm_own_entry. b = ff_q_gcrt_gfull_normalized_unique_left_lcm_own_entry * S ((S (gcrt_common_index_gfull_normalized_unique_left_lcm_own)) * c) + (gcrt_common_modulus_gfull_normalized_unique_left_lcm_own))) -> exists gcrt_common_quotient_gfull_normalized_unique_left_lcm_own. M = gcrt_common_modulus_gfull_normalized_unique_left_lcm_own * gcrt_common_quotient_gfull_normalized_unique_left_lcm_own) /\ forall gcrt_lcm_common_gfull_normalized_unique_left_lcm. (forall gcrt_common_index_gfull_normalized_unique_left_lcm_other gcrt_common_modulus_gfull_normalized_unique_left_lcm_other. (exists ff_lt_gcrt_gfull_normalized_unique_left_lcm_other_bound. ff_lt_gcrt_gfull_normalized_unique_left_lcm_other_bound + S gcrt_common_index_gfull_normalized_unique_left_lcm_other = l) -> (((exists ff_h_gcrt_gfull_normalized_unique_left_lcm_other_entry. ff_h_gcrt_gfull_normalized_unique_left_lcm_other_entry + S (gcrt_common_modulus_gfull_normalized_unique_left_lcm_other) = S ((S (gcrt_common_index_gfull_normalized_unique_left_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_normalized_unique_left_lcm_other_entry. b = ff_q_gcrt_gfull_normalized_unique_left_lcm_other_entry * S ((S (gcrt_common_index_gfull_normalized_unique_left_lcm_other)) * c) + (gcrt_common_modulus_gfull_normalized_unique_left_lcm_other))) -> exists gcrt_common_quotient_gfull_normalized_unique_left_lcm_other. gcrt_lcm_common_gfull_normalized_unique_left_lcm = gcrt_common_modulus_gfull_normalized_unique_left_lcm_other * gcrt_common_quotient_gfull_normalized_unique_left_lcm_other) -> exists gcrt_lcm_quotient_gfull_normalized_unique_left_lcm. gcrt_lcm_common_gfull_normalized_unique_left_lcm = M * gcrt_lcm_quotient_gfull_normalized_unique_left_lcm)) /\ ((M = 0 \/ (exists ff_lt_gcrt_gfull_normalized_unique_left_bound. ff_lt_gcrt_gfull_normalized_unique_left_bound + S x = M)) /\ (forall gcrt_solution_index_gfull_normalized_unique_left_solution gcrt_solution_residue_gfull_normalized_unique_left_solution gcrt_solution_modulus_gfull_normalized_unique_left_solution. (exists ff_lt_gcrt_gfull_normalized_unique_left_solution_bound. ff_lt_gcrt_gfull_normalized_unique_left_solution_bound + S gcrt_solution_index_gfull_normalized_unique_left_solution = l) -> (((exists ff_h_gcrt_gfull_normalized_unique_left_solution_residue. ff_h_gcrt_gfull_normalized_unique_left_solution_residue + S (gcrt_solution_residue_gfull_normalized_unique_left_solution) = S ((S (gcrt_solution_index_gfull_normalized_unique_left_solution)) * s)) /\ exists ff_q_gcrt_gfull_normalized_unique_left_solution_residue. r = ff_q_gcrt_gfull_normalized_unique_left_solution_residue * S ((S (gcrt_solution_index_gfull_normalized_unique_left_solution)) * s) + (gcrt_solution_residue_gfull_normalized_unique_left_solution))) -> (((exists ff_h_gcrt_gfull_normalized_unique_left_solution_modulus. ff_h_gcrt_gfull_normalized_unique_left_solution_modulus + S (gcrt_solution_modulus_gfull_normalized_unique_left_solution) = S ((S (gcrt_solution_index_gfull_normalized_unique_left_solution)) * c)) /\ exists ff_q_gcrt_gfull_normalized_unique_left_solution_modulus. b = ff_q_gcrt_gfull_normalized_unique_left_solution_modulus * S ((S (gcrt_solution_index_gfull_normalized_unique_left_solution)) * c) + (gcrt_solution_modulus_gfull_normalized_unique_left_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_unique_left_solution_congruence hgcrt_mod_right_gcrt_gfull_normalized_unique_left_solution_congruence. x + gcrt_solution_modulus_gfull_normalized_unique_left_solution * hgcrt_mod_left_gcrt_gfull_normalized_unique_left_solution_congruence = gcrt_solution_residue_gfull_normalized_unique_left_solution + gcrt_solution_modulus_gfull_normalized_unique_left_solution * hgcrt_mod_right_gcrt_gfull_normalized_unique_left_solution_congruence))))) -> (((((forall gcrt_common_index_gfull_normalized_unique_right_lcm_own gcrt_common_modulus_gfull_normalized_unique_right_lcm_own. (exists ff_lt_gcrt_gfull_normalized_unique_right_lcm_own_bound. ff_lt_gcrt_gfull_normalized_unique_right_lcm_own_bound + S gcrt_common_index_gfull_normalized_unique_right_lcm_own = l) -> (((exists ff_h_gcrt_gfull_normalized_unique_right_lcm_own_entry. ff_h_gcrt_gfull_normalized_unique_right_lcm_own_entry + S (gcrt_common_modulus_gfull_normalized_unique_right_lcm_own) = S ((S (gcrt_common_index_gfull_normalized_unique_right_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_normalized_unique_right_lcm_own_entry. b = ff_q_gcrt_gfull_normalized_unique_right_lcm_own_entry * S ((S (gcrt_common_index_gfull_normalized_unique_right_lcm_own)) * c) + (gcrt_common_modulus_gfull_normalized_unique_right_lcm_own))) -> exists gcrt_common_quotient_gfull_normalized_unique_right_lcm_own. M = gcrt_common_modulus_gfull_normalized_unique_right_lcm_own * gcrt_common_quotient_gfull_normalized_unique_right_lcm_own) /\ forall gcrt_lcm_common_gfull_normalized_unique_right_lcm. (forall gcrt_common_index_gfull_normalized_unique_right_lcm_other gcrt_common_modulus_gfull_normalized_unique_right_lcm_other. (exists ff_lt_gcrt_gfull_normalized_unique_right_lcm_other_bound. ff_lt_gcrt_gfull_normalized_unique_right_lcm_other_bound + S gcrt_common_index_gfull_normalized_unique_right_lcm_other = l) -> (((exists ff_h_gcrt_gfull_normalized_unique_right_lcm_other_entry. ff_h_gcrt_gfull_normalized_unique_right_lcm_other_entry + S (gcrt_common_modulus_gfull_normalized_unique_right_lcm_other) = S ((S (gcrt_common_index_gfull_normalized_unique_right_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_normalized_unique_right_lcm_other_entry. b = ff_q_gcrt_gfull_normalized_unique_right_lcm_other_entry * S ((S (gcrt_common_index_gfull_normalized_unique_right_lcm_other)) * c) + (gcrt_common_modulus_gfull_normalized_unique_right_lcm_other))) -> exists gcrt_common_quotient_gfull_normalized_unique_right_lcm_other. gcrt_lcm_common_gfull_normalized_unique_right_lcm = gcrt_common_modulus_gfull_normalized_unique_right_lcm_other * gcrt_common_quotient_gfull_normalized_unique_right_lcm_other) -> exists gcrt_lcm_quotient_gfull_normalized_unique_right_lcm. gcrt_lcm_common_gfull_normalized_unique_right_lcm = M * gcrt_lcm_quotient_gfull_normalized_unique_right_lcm)) /\ ((M = 0 \/ (exists ff_lt_gcrt_gfull_normalized_unique_right_bound. ff_lt_gcrt_gfull_normalized_unique_right_bound + S y = M)) /\ (forall gcrt_solution_index_gfull_normalized_unique_right_solution gcrt_solution_residue_gfull_normalized_unique_right_solution gcrt_solution_modulus_gfull_normalized_unique_right_solution. (exists ff_lt_gcrt_gfull_normalized_unique_right_solution_bound. ff_lt_gcrt_gfull_normalized_unique_right_solution_bound + S gcrt_solution_index_gfull_normalized_unique_right_solution = l) -> (((exists ff_h_gcrt_gfull_normalized_unique_right_solution_residue. ff_h_gcrt_gfull_normalized_unique_right_solution_residue + S (gcrt_solution_residue_gfull_normalized_unique_right_solution) = S ((S (gcrt_solution_index_gfull_normalized_unique_right_solution)) * s)) /\ exists ff_q_gcrt_gfull_normalized_unique_right_solution_residue. r = ff_q_gcrt_gfull_normalized_unique_right_solution_residue * S ((S (gcrt_solution_index_gfull_normalized_unique_right_solution)) * s) + (gcrt_solution_residue_gfull_normalized_unique_right_solution))) -> (((exists ff_h_gcrt_gfull_normalized_unique_right_solution_modulus. ff_h_gcrt_gfull_normalized_unique_right_solution_modulus + S (gcrt_solution_modulus_gfull_normalized_unique_right_solution) = S ((S (gcrt_solution_index_gfull_normalized_unique_right_solution)) * c)) /\ exists ff_q_gcrt_gfull_normalized_unique_right_solution_modulus. b = ff_q_gcrt_gfull_normalized_unique_right_solution_modulus * S ((S (gcrt_solution_index_gfull_normalized_unique_right_solution)) * c) + (gcrt_solution_modulus_gfull_normalized_unique_right_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_unique_right_solution_congruence hgcrt_mod_right_gcrt_gfull_normalized_unique_right_solution_congruence. y + gcrt_solution_modulus_gfull_normalized_unique_right_solution * hgcrt_mod_left_gcrt_gfull_normalized_unique_right_solution_congruence = gcrt_solution_residue_gfull_normalized_unique_right_solution + gcrt_solution_modulus_gfull_normalized_unique_right_solution * hgcrt_mod_right_gcrt_gfull_normalized_unique_right_solution_congruence))))) -> y = x

Complete tactic proof in conservative notation

All 61 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

61 script commands · 16 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 M
  7. L7
    intro x
  8. L8
    intro y
  9. L9
    intro hx
  10. L10
    intro hy
02Separate the logical casesL11–15

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
  5. L15
    cases hx_right_left
03Use earlier factsL16–25

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

  1. L16
    specialize crt_prefix_zero_lcm_solution_unique r
  2. L17
    specialize crt_prefix_zero_lcm_solution_unique s
  3. L18
    specialize crt_prefix_zero_lcm_solution_unique b
  4. L19
    specialize crt_prefix_zero_lcm_solution_unique c
  5. L20
    specialize crt_prefix_zero_lcm_solution_unique l
  6. L21
    specialize crt_prefix_zero_lcm_solution_unique M
  7. L22
    specialize crt_prefix_zero_lcm_solution_unique x
  8. L23
    specialize crt_prefix_zero_lcm_solution_unique y
  9. L24
    apply crt_prefix_zero_lcm_solution_unique
  10. L25
    exact hx_left
04Use earlier factsL26–28

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

  1. L26
    exact hx_right_left_left
  2. L27
    exact hx_right_right
  3. L28
    exact hy_right_right
05Separate the logical casesL29–29

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

  1. L29
    cases hy_right_left
06Use earlier factsL30–39

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

  1. L30
    specialize crt_prefix_zero_lcm_solution_unique r
  2. L31
    specialize crt_prefix_zero_lcm_solution_unique s
  3. L32
    specialize crt_prefix_zero_lcm_solution_unique b
  4. L33
    specialize crt_prefix_zero_lcm_solution_unique c
  5. L34
    specialize crt_prefix_zero_lcm_solution_unique l
  6. L35
    specialize crt_prefix_zero_lcm_solution_unique M
  7. L36
    specialize crt_prefix_zero_lcm_solution_unique x
  8. L37
    specialize crt_prefix_zero_lcm_solution_unique y
  9. L38
    apply crt_prefix_zero_lcm_solution_unique
  10. L39
    exact hx_left
07Use earlier factsL40–49

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

  1. L40
    exact hy_right_left_left
  2. L41
    exact hx_right_right
  3. L42
    exact hy_right_right
  4. L43
    specialize crt_canonical_prefix_solution_unique r
  5. L44
    specialize crt_canonical_prefix_solution_unique s
  6. L45
    specialize crt_canonical_prefix_solution_unique b
  7. L46
    specialize crt_canonical_prefix_solution_unique c
  8. L47
    specialize crt_canonical_prefix_solution_unique l
  9. L48
    specialize crt_canonical_prefix_solution_unique M
  10. L49
    specialize crt_canonical_prefix_solution_unique x
08Use earlier factsL50–51

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

  1. L50
    specialize crt_canonical_prefix_solution_unique y
  2. L51
    apply crt_canonical_prefix_solution_unique
09Separate the logical casesL52–52

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

  1. L52
    split
10Use earlier factsL53–53

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

  1. L53
    exact hx_left
11Separate the logical casesL54–54

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

  1. L54
    split
12Use earlier factsL55–56

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

  1. L55
    exact hx_right_left_right
  2. L56
    exact hx_right_right
13Separate the logical casesL57–57

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

  1. L57
    split
14Use earlier factsL58–58

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

  1. L58
    exact hy_left
15Separate the logical casesL59–59

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

  1. L59
    split
16Use earlier factsL60–61

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

  1. L60
    exact hy_right_left_right
  2. L61
    exact hy_right_right

Library-wide reading audit

Original defined command ledger · 61 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. 0015cases hx_right_left
  16. 0016specialize crt_prefix_zero_lcm_solution_unique r
  17. 0017specialize crt_prefix_zero_lcm_solution_unique s
  18. 0018specialize crt_prefix_zero_lcm_solution_unique b
  19. 0019specialize crt_prefix_zero_lcm_solution_unique c
  20. 0020specialize crt_prefix_zero_lcm_solution_unique l
  21. 0021specialize crt_prefix_zero_lcm_solution_unique M
  22. 0022specialize crt_prefix_zero_lcm_solution_unique x
  23. 0023specialize crt_prefix_zero_lcm_solution_unique y
  24. 0024apply crt_prefix_zero_lcm_solution_unique
  25. 0025exact hx_left
  26. 0026exact hx_right_left_left
  27. 0027exact hx_right_right
  28. 0028exact hy_right_right
  29. 0029cases hy_right_left
  30. 0030specialize crt_prefix_zero_lcm_solution_unique r
  31. 0031specialize crt_prefix_zero_lcm_solution_unique s
  32. 0032specialize crt_prefix_zero_lcm_solution_unique b
  33. 0033specialize crt_prefix_zero_lcm_solution_unique c
  34. 0034specialize crt_prefix_zero_lcm_solution_unique l
  35. 0035specialize crt_prefix_zero_lcm_solution_unique M
  36. 0036specialize crt_prefix_zero_lcm_solution_unique x
  37. 0037specialize crt_prefix_zero_lcm_solution_unique y
  38. 0038apply crt_prefix_zero_lcm_solution_unique
  39. 0039exact hx_left
  40. 0040exact hy_right_left_left
  41. 0041exact hx_right_right
  42. 0042exact hy_right_right
  43. 0043specialize crt_canonical_prefix_solution_unique r
  44. 0044specialize crt_canonical_prefix_solution_unique s
  45. 0045specialize crt_canonical_prefix_solution_unique b
  46. 0046specialize crt_canonical_prefix_solution_unique c
  47. 0047specialize crt_canonical_prefix_solution_unique l
  48. 0048specialize crt_canonical_prefix_solution_unique M
  49. 0049specialize crt_canonical_prefix_solution_unique x
  50. 0050specialize crt_canonical_prefix_solution_unique y
  51. 0051apply crt_canonical_prefix_solution_unique
  52. 0052split
  53. 0053exact hx_left
  54. 0054split
  55. 0055exact hx_right_left_right
  56. 0056exact hx_right_right
  57. 0057split
  58. 0058exact hy_left
  59. 0059split
  60. 0060exact hy_right_left_right
  61. 0061exact hy_right_right