FC0017

crt_normalized_zero_lcm_all_solutions_unique

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

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

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

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

crt_prefix_zero_lcm_solution_unique Alpha theorem; checked-use authorized

Direct dependents

none

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

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.

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