CR000D

crt_prefix_lcm_unique

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 1 declared prerequisite and contains 18 exact native proof lines.

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

Proof neighborhood

Direct dependencies

multiple_antisymm Stable theorem; checked-use authorized

Direct dependents

CR0010 crt_prefix_lcm_exists_unique CR0011 crt_pairwise_coprime_prefix_lcm_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

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.

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

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