FC0017

crt_normalized_zero_lcm_all_solutions_unique

At zero list LCM every actual simultaneous solution equals the normalized one; no bound or normalization premise is imposed on the comparison solution.

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

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

Definition DAG

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

Actual proof prerequisites

crt_prefix_zero_lcm_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_zero_source_lcm_own gcrt_common_modulus_gfull_normalized_zero_source_lcm_own. (exists ff_lt_gcrt_gfull_normalized_zero_source_lcm_own_bound. ff_lt_gcrt_gfull_normalized_zero_source_lcm_own_bound + S gcrt_common_index_gfull_normalized_zero_source_lcm_own = l) -> (((exists ff_h_gcrt_gfull_normalized_zero_source_lcm_own_entry. ff_h_gcrt_gfull_normalized_zero_source_lcm_own_entry + S (gcrt_common_modulus_gfull_normalized_zero_source_lcm_own) = S ((S (gcrt_common_index_gfull_normalized_zero_source_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_normalized_zero_source_lcm_own_entry. b = ff_q_gcrt_gfull_normalized_zero_source_lcm_own_entry * S ((S (gcrt_common_index_gfull_normalized_zero_source_lcm_own)) * c) + (gcrt_common_modulus_gfull_normalized_zero_source_lcm_own))) -> exists gcrt_common_quotient_gfull_normalized_zero_source_lcm_own. M = gcrt_common_modulus_gfull_normalized_zero_source_lcm_own * gcrt_common_quotient_gfull_normalized_zero_source_lcm_own) /\ forall gcrt_lcm_common_gfull_normalized_zero_source_lcm. (forall gcrt_common_index_gfull_normalized_zero_source_lcm_other gcrt_common_modulus_gfull_normalized_zero_source_lcm_other. (exists ff_lt_gcrt_gfull_normalized_zero_source_lcm_other_bound. ff_lt_gcrt_gfull_normalized_zero_source_lcm_other_bound + S gcrt_common_index_gfull_normalized_zero_source_lcm_other = l) -> (((exists ff_h_gcrt_gfull_normalized_zero_source_lcm_other_entry. ff_h_gcrt_gfull_normalized_zero_source_lcm_other_entry + S (gcrt_common_modulus_gfull_normalized_zero_source_lcm_other) = S ((S (gcrt_common_index_gfull_normalized_zero_source_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_normalized_zero_source_lcm_other_entry. b = ff_q_gcrt_gfull_normalized_zero_source_lcm_other_entry * S ((S (gcrt_common_index_gfull_normalized_zero_source_lcm_other)) * c) + (gcrt_common_modulus_gfull_normalized_zero_source_lcm_other))) -> exists gcrt_common_quotient_gfull_normalized_zero_source_lcm_other. gcrt_lcm_common_gfull_normalized_zero_source_lcm = gcrt_common_modulus_gfull_normalized_zero_source_lcm_other * gcrt_common_quotient_gfull_normalized_zero_source_lcm_other) -> exists gcrt_lcm_quotient_gfull_normalized_zero_source_lcm. gcrt_lcm_common_gfull_normalized_zero_source_lcm = M * gcrt_lcm_quotient_gfull_normalized_zero_source_lcm)) /\ ((M = 0 \/ (exists ff_lt_gcrt_gfull_normalized_zero_source_bound. ff_lt_gcrt_gfull_normalized_zero_source_bound + S x = M)) /\ (forall gcrt_solution_index_gfull_normalized_zero_source_solution gcrt_solution_residue_gfull_normalized_zero_source_solution gcrt_solution_modulus_gfull_normalized_zero_source_solution. (exists ff_lt_gcrt_gfull_normalized_zero_source_solution_bound. ff_lt_gcrt_gfull_normalized_zero_source_solution_bound + S gcrt_solution_index_gfull_normalized_zero_source_solution = l) -> (((exists ff_h_gcrt_gfull_normalized_zero_source_solution_residue. ff_h_gcrt_gfull_normalized_zero_source_solution_residue + S (gcrt_solution_residue_gfull_normalized_zero_source_solution) = S ((S (gcrt_solution_index_gfull_normalized_zero_source_solution)) * s)) /\ exists ff_q_gcrt_gfull_normalized_zero_source_solution_residue. r = ff_q_gcrt_gfull_normalized_zero_source_solution_residue * S ((S (gcrt_solution_index_gfull_normalized_zero_source_solution)) * s) + (gcrt_solution_residue_gfull_normalized_zero_source_solution))) -> (((exists ff_h_gcrt_gfull_normalized_zero_source_solution_modulus. ff_h_gcrt_gfull_normalized_zero_source_solution_modulus + S (gcrt_solution_modulus_gfull_normalized_zero_source_solution) = S ((S (gcrt_solution_index_gfull_normalized_zero_source_solution)) * c)) /\ exists ff_q_gcrt_gfull_normalized_zero_source_solution_modulus. b = ff_q_gcrt_gfull_normalized_zero_source_solution_modulus * S ((S (gcrt_solution_index_gfull_normalized_zero_source_solution)) * c) + (gcrt_solution_modulus_gfull_normalized_zero_source_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_zero_source_solution_congruence hgcrt_mod_right_gcrt_gfull_normalized_zero_source_solution_congruence. x + gcrt_solution_modulus_gfull_normalized_zero_source_solution * hgcrt_mod_left_gcrt_gfull_normalized_zero_source_solution_congruence = gcrt_solution_residue_gfull_normalized_zero_source_solution + gcrt_solution_modulus_gfull_normalized_zero_source_solution * hgcrt_mod_right_gcrt_gfull_normalized_zero_source_solution_congruence))))) -> M = 0 -> (forall gcrt_solution_index_gfull_normalized_zero_compared gcrt_solution_residue_gfull_normalized_zero_compared gcrt_solution_modulus_gfull_normalized_zero_compared. (exists ff_lt_gcrt_gfull_normalized_zero_compared_bound. ff_lt_gcrt_gfull_normalized_zero_compared_bound + S gcrt_solution_index_gfull_normalized_zero_compared = l) -> (((exists ff_h_gcrt_gfull_normalized_zero_compared_residue. ff_h_gcrt_gfull_normalized_zero_compared_residue + S (gcrt_solution_residue_gfull_normalized_zero_compared) = S ((S (gcrt_solution_index_gfull_normalized_zero_compared)) * s)) /\ exists ff_q_gcrt_gfull_normalized_zero_compared_residue. r = ff_q_gcrt_gfull_normalized_zero_compared_residue * S ((S (gcrt_solution_index_gfull_normalized_zero_compared)) * s) + (gcrt_solution_residue_gfull_normalized_zero_compared))) -> (((exists ff_h_gcrt_gfull_normalized_zero_compared_modulus. ff_h_gcrt_gfull_normalized_zero_compared_modulus + S (gcrt_solution_modulus_gfull_normalized_zero_compared) = S ((S (gcrt_solution_index_gfull_normalized_zero_compared)) * c)) /\ exists ff_q_gcrt_gfull_normalized_zero_compared_modulus. b = ff_q_gcrt_gfull_normalized_zero_compared_modulus * S ((S (gcrt_solution_index_gfull_normalized_zero_compared)) * c) + (gcrt_solution_modulus_gfull_normalized_zero_compared))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_zero_compared_congruence hgcrt_mod_right_gcrt_gfull_normalized_zero_compared_congruence. y + gcrt_solution_modulus_gfull_normalized_zero_compared * hgcrt_mod_left_gcrt_gfull_normalized_zero_compared_congruence = gcrt_solution_residue_gfull_normalized_zero_compared + gcrt_solution_modulus_gfull_normalized_zero_compared * hgcrt_mod_right_gcrt_gfull_normalized_zero_compared_congruence)) -> y = x

Complete tactic proof in conservative notation

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

26 script commands · 5 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 hzero
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hy
03Separate the logical casesL12–13

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

  1. L12
    cases hx
  2. L13
    cases hx_right
04Use earlier factsL14–23

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

  1. L14
    specialize crt_prefix_zero_lcm_solution_unique r
  2. L15
    specialize crt_prefix_zero_lcm_solution_unique s
  3. L16
    specialize crt_prefix_zero_lcm_solution_unique b
  4. L17
    specialize crt_prefix_zero_lcm_solution_unique c
  5. L18
    specialize crt_prefix_zero_lcm_solution_unique l
  6. L19
    specialize crt_prefix_zero_lcm_solution_unique M
  7. L20
    specialize crt_prefix_zero_lcm_solution_unique x
  8. L21
    specialize crt_prefix_zero_lcm_solution_unique y
  9. L22
    apply crt_prefix_zero_lcm_solution_unique
  10. L23
    exact hx_left
05Use earlier factsL24–26

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

  1. L24
    exact hzero
  2. L25
    exact hx_right_right
  3. L26
    exact hy

Library-wide reading audit

Original defined command ledger · 26 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 hzero
  11. 0011intro hy
  12. 0012cases hx
  13. 0013cases hx_right
  14. 0014specialize crt_prefix_zero_lcm_solution_unique r
  15. 0015specialize crt_prefix_zero_lcm_solution_unique s
  16. 0016specialize crt_prefix_zero_lcm_solution_unique b
  17. 0017specialize crt_prefix_zero_lcm_solution_unique c
  18. 0018specialize crt_prefix_zero_lcm_solution_unique l
  19. 0019specialize crt_prefix_zero_lcm_solution_unique M
  20. 0020specialize crt_prefix_zero_lcm_solution_unique x
  21. 0021specialize crt_prefix_zero_lcm_solution_unique y
  22. 0022apply crt_prefix_zero_lcm_solution_unique
  23. 0023exact hx_left
  24. 0024exact hzero
  25. 0025exact hx_right_right
  26. 0026exact hy