CR000D

crt_prefix_lcm_unique

The universal-property lcm of any decoded finite modulus prefix is unique whenever it exists.

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

∀ b. ∀ c. ∀ l. ∀ x. ∀ y. CRTPrefixLCM(b,c,l,x) → CRTPrefixLCM(b,c,l,y) → x = y

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

Definition DAG

CRTPrefixLCM(b,c,l,M) · 2

Actual proof prerequisites

multiple_antisymm · checked external prerequisite
Original expanded first-order statement 
forall b c l x y. (((forall gcrt_common_index_lcm_unique_left_own gcrt_common_modulus_lcm_unique_left_own. (exists ff_lt_gcrt_lcm_unique_left_own_bound. ff_lt_gcrt_lcm_unique_left_own_bound + S gcrt_common_index_lcm_unique_left_own = l) -> (((exists ff_h_gcrt_lcm_unique_left_own_entry. ff_h_gcrt_lcm_unique_left_own_entry + S (gcrt_common_modulus_lcm_unique_left_own) = S ((S (gcrt_common_index_lcm_unique_left_own)) * c)) /\ exists ff_q_gcrt_lcm_unique_left_own_entry. b = ff_q_gcrt_lcm_unique_left_own_entry * S ((S (gcrt_common_index_lcm_unique_left_own)) * c) + (gcrt_common_modulus_lcm_unique_left_own))) -> exists gcrt_common_quotient_lcm_unique_left_own. x = gcrt_common_modulus_lcm_unique_left_own * gcrt_common_quotient_lcm_unique_left_own) /\ forall gcrt_lcm_common_lcm_unique_left. (forall gcrt_common_index_lcm_unique_left_other gcrt_common_modulus_lcm_unique_left_other. (exists ff_lt_gcrt_lcm_unique_left_other_bound. ff_lt_gcrt_lcm_unique_left_other_bound + S gcrt_common_index_lcm_unique_left_other = l) -> (((exists ff_h_gcrt_lcm_unique_left_other_entry. ff_h_gcrt_lcm_unique_left_other_entry + S (gcrt_common_modulus_lcm_unique_left_other) = S ((S (gcrt_common_index_lcm_unique_left_other)) * c)) /\ exists ff_q_gcrt_lcm_unique_left_other_entry. b = ff_q_gcrt_lcm_unique_left_other_entry * S ((S (gcrt_common_index_lcm_unique_left_other)) * c) + (gcrt_common_modulus_lcm_unique_left_other))) -> exists gcrt_common_quotient_lcm_unique_left_other. gcrt_lcm_common_lcm_unique_left = gcrt_common_modulus_lcm_unique_left_other * gcrt_common_quotient_lcm_unique_left_other) -> exists gcrt_lcm_quotient_lcm_unique_left. gcrt_lcm_common_lcm_unique_left = x * gcrt_lcm_quotient_lcm_unique_left)) -> (((forall gcrt_common_index_lcm_unique_right_own gcrt_common_modulus_lcm_unique_right_own. (exists ff_lt_gcrt_lcm_unique_right_own_bound. ff_lt_gcrt_lcm_unique_right_own_bound + S gcrt_common_index_lcm_unique_right_own = l) -> (((exists ff_h_gcrt_lcm_unique_right_own_entry. ff_h_gcrt_lcm_unique_right_own_entry + S (gcrt_common_modulus_lcm_unique_right_own) = S ((S (gcrt_common_index_lcm_unique_right_own)) * c)) /\ exists ff_q_gcrt_lcm_unique_right_own_entry. b = ff_q_gcrt_lcm_unique_right_own_entry * S ((S (gcrt_common_index_lcm_unique_right_own)) * c) + (gcrt_common_modulus_lcm_unique_right_own))) -> exists gcrt_common_quotient_lcm_unique_right_own. y = gcrt_common_modulus_lcm_unique_right_own * gcrt_common_quotient_lcm_unique_right_own) /\ forall gcrt_lcm_common_lcm_unique_right. (forall gcrt_common_index_lcm_unique_right_other gcrt_common_modulus_lcm_unique_right_other. (exists ff_lt_gcrt_lcm_unique_right_other_bound. ff_lt_gcrt_lcm_unique_right_other_bound + S gcrt_common_index_lcm_unique_right_other = l) -> (((exists ff_h_gcrt_lcm_unique_right_other_entry. ff_h_gcrt_lcm_unique_right_other_entry + S (gcrt_common_modulus_lcm_unique_right_other) = S ((S (gcrt_common_index_lcm_unique_right_other)) * c)) /\ exists ff_q_gcrt_lcm_unique_right_other_entry. b = ff_q_gcrt_lcm_unique_right_other_entry * S ((S (gcrt_common_index_lcm_unique_right_other)) * c) + (gcrt_common_modulus_lcm_unique_right_other))) -> exists gcrt_common_quotient_lcm_unique_right_other. gcrt_lcm_common_lcm_unique_right = gcrt_common_modulus_lcm_unique_right_other * gcrt_common_quotient_lcm_unique_right_other) -> exists gcrt_lcm_quotient_lcm_unique_right. gcrt_lcm_common_lcm_unique_right = y * gcrt_lcm_quotient_lcm_unique_right)) -> x = y

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

18 script commands · 3 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–7

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro x
  5. L5
    intro y
  6. L6
    intro hx
  7. L7
    intro hy
02Separate the logical casesL8–9

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

  1. L8
    cases hx
  2. L9
    cases hy
03Use earlier factsL10–18

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

  1. L10
    specialize multiple_antisymm x
  2. L11
    specialize multiple_antisymm y
  3. L12
    apply multiple_antisymm
  4. L13
    specialize hx_right y
  5. L14
    apply hx_right
  6. L15
    exact hy_left
  7. L16
    specialize hy_right x
  8. L17
    apply hy_right
  9. L18
    exact hx_left

Library-wide reading audit

Original defined command ledger · 18 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro x
  5. 0005intro y
  6. 0006intro hx
  7. 0007intro hy
  8. 0008cases hx
  9. 0009cases hy
  10. 0010specialize multiple_antisymm x
  11. 0011specialize multiple_antisymm y
  12. 0012apply multiple_antisymm
  13. 0013specialize hx_right y
  14. 0014apply hx_right
  15. 0015exact hy_left
  16. 0016specialize hy_right x
  17. 0017apply hy_right
  18. 0018exact hx_left