GC000B

crt_prefix_zero_lcm_solution_unique

At list LCM zero, every simultaneous solution of an arbitrary decoded congruence system is literally unique.

Alpha v34 checked-use · first admitted v25 · 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 under successive-merge compatibility and in the pairwise-compatible dominating-last case. G011 is now closed in the separate Alpha-v27 generalized-crt branch for arbitrary pairwise-compatible finite lists, including noncoprime moduli. Full G011 proof · Alpha v27

Exact theorem in conservative defined notation

∀ r. ∀ s. ∀ b. ∀ c. ∀ l. ∀ M. ∀ x. ∀ y. CRTPrefixLCM(b,c,l,M) → M = 0 → CRTPrefixSolution(r,s,b,c,l,x) → 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) · 2CRTPrefixLCM(b,c,l,M) · 1

Actual proof prerequisites

crt_prefix_solutions_congruent_lcm · checked external prerequisitemod_eq_zero_iff_eq · checked external prerequisite
Original expanded first-order statement 
forall r s b c l M x y. (((forall gcrt_common_index_gcomp_zero_lcm_source_own gcrt_common_modulus_gcomp_zero_lcm_source_own. (exists ff_lt_gcrt_gcomp_zero_lcm_source_own_bound. ff_lt_gcrt_gcomp_zero_lcm_source_own_bound + S gcrt_common_index_gcomp_zero_lcm_source_own = l) -> (((exists ff_h_gcrt_gcomp_zero_lcm_source_own_entry. ff_h_gcrt_gcomp_zero_lcm_source_own_entry + S (gcrt_common_modulus_gcomp_zero_lcm_source_own) = S ((S (gcrt_common_index_gcomp_zero_lcm_source_own)) * c)) /\ exists ff_q_gcrt_gcomp_zero_lcm_source_own_entry. b = ff_q_gcrt_gcomp_zero_lcm_source_own_entry * S ((S (gcrt_common_index_gcomp_zero_lcm_source_own)) * c) + (gcrt_common_modulus_gcomp_zero_lcm_source_own))) -> exists gcrt_common_quotient_gcomp_zero_lcm_source_own. M = gcrt_common_modulus_gcomp_zero_lcm_source_own * gcrt_common_quotient_gcomp_zero_lcm_source_own) /\ forall gcrt_lcm_common_gcomp_zero_lcm_source. (forall gcrt_common_index_gcomp_zero_lcm_source_other gcrt_common_modulus_gcomp_zero_lcm_source_other. (exists ff_lt_gcrt_gcomp_zero_lcm_source_other_bound. ff_lt_gcrt_gcomp_zero_lcm_source_other_bound + S gcrt_common_index_gcomp_zero_lcm_source_other = l) -> (((exists ff_h_gcrt_gcomp_zero_lcm_source_other_entry. ff_h_gcrt_gcomp_zero_lcm_source_other_entry + S (gcrt_common_modulus_gcomp_zero_lcm_source_other) = S ((S (gcrt_common_index_gcomp_zero_lcm_source_other)) * c)) /\ exists ff_q_gcrt_gcomp_zero_lcm_source_other_entry. b = ff_q_gcrt_gcomp_zero_lcm_source_other_entry * S ((S (gcrt_common_index_gcomp_zero_lcm_source_other)) * c) + (gcrt_common_modulus_gcomp_zero_lcm_source_other))) -> exists gcrt_common_quotient_gcomp_zero_lcm_source_other. gcrt_lcm_common_gcomp_zero_lcm_source = gcrt_common_modulus_gcomp_zero_lcm_source_other * gcrt_common_quotient_gcomp_zero_lcm_source_other) -> exists gcrt_lcm_quotient_gcomp_zero_lcm_source. gcrt_lcm_common_gcomp_zero_lcm_source = M * gcrt_lcm_quotient_gcomp_zero_lcm_source)) -> M = 0 -> (forall gcrt_solution_index_gcomp_zero_solution_left gcrt_solution_residue_gcomp_zero_solution_left gcrt_solution_modulus_gcomp_zero_solution_left. (exists ff_lt_gcrt_gcomp_zero_solution_left_bound. ff_lt_gcrt_gcomp_zero_solution_left_bound + S gcrt_solution_index_gcomp_zero_solution_left = l) -> (((exists ff_h_gcrt_gcomp_zero_solution_left_residue. ff_h_gcrt_gcomp_zero_solution_left_residue + S (gcrt_solution_residue_gcomp_zero_solution_left) = S ((S (gcrt_solution_index_gcomp_zero_solution_left)) * s)) /\ exists ff_q_gcrt_gcomp_zero_solution_left_residue. r = ff_q_gcrt_gcomp_zero_solution_left_residue * S ((S (gcrt_solution_index_gcomp_zero_solution_left)) * s) + (gcrt_solution_residue_gcomp_zero_solution_left))) -> (((exists ff_h_gcrt_gcomp_zero_solution_left_modulus. ff_h_gcrt_gcomp_zero_solution_left_modulus + S (gcrt_solution_modulus_gcomp_zero_solution_left) = S ((S (gcrt_solution_index_gcomp_zero_solution_left)) * c)) /\ exists ff_q_gcrt_gcomp_zero_solution_left_modulus. b = ff_q_gcrt_gcomp_zero_solution_left_modulus * S ((S (gcrt_solution_index_gcomp_zero_solution_left)) * c) + (gcrt_solution_modulus_gcomp_zero_solution_left))) -> (exists hgcrt_mod_left_gcrt_gcomp_zero_solution_left_congruence hgcrt_mod_right_gcrt_gcomp_zero_solution_left_congruence. x + gcrt_solution_modulus_gcomp_zero_solution_left * hgcrt_mod_left_gcrt_gcomp_zero_solution_left_congruence = gcrt_solution_residue_gcomp_zero_solution_left + gcrt_solution_modulus_gcomp_zero_solution_left * hgcrt_mod_right_gcrt_gcomp_zero_solution_left_congruence)) -> (forall gcrt_solution_index_gcomp_zero_solution_right gcrt_solution_residue_gcomp_zero_solution_right gcrt_solution_modulus_gcomp_zero_solution_right. (exists ff_lt_gcrt_gcomp_zero_solution_right_bound. ff_lt_gcrt_gcomp_zero_solution_right_bound + S gcrt_solution_index_gcomp_zero_solution_right = l) -> (((exists ff_h_gcrt_gcomp_zero_solution_right_residue. ff_h_gcrt_gcomp_zero_solution_right_residue + S (gcrt_solution_residue_gcomp_zero_solution_right) = S ((S (gcrt_solution_index_gcomp_zero_solution_right)) * s)) /\ exists ff_q_gcrt_gcomp_zero_solution_right_residue. r = ff_q_gcrt_gcomp_zero_solution_right_residue * S ((S (gcrt_solution_index_gcomp_zero_solution_right)) * s) + (gcrt_solution_residue_gcomp_zero_solution_right))) -> (((exists ff_h_gcrt_gcomp_zero_solution_right_modulus. ff_h_gcrt_gcomp_zero_solution_right_modulus + S (gcrt_solution_modulus_gcomp_zero_solution_right) = S ((S (gcrt_solution_index_gcomp_zero_solution_right)) * c)) /\ exists ff_q_gcrt_gcomp_zero_solution_right_modulus. b = ff_q_gcrt_gcomp_zero_solution_right_modulus * S ((S (gcrt_solution_index_gcomp_zero_solution_right)) * c) + (gcrt_solution_modulus_gcomp_zero_solution_right))) -> (exists hgcrt_mod_left_gcrt_gcomp_zero_solution_right_congruence hgcrt_mod_right_gcrt_gcomp_zero_solution_right_congruence. y + gcrt_solution_modulus_gcomp_zero_solution_right * hgcrt_mod_left_gcrt_gcomp_zero_solution_right_congruence = gcrt_solution_residue_gcomp_zero_solution_right + gcrt_solution_modulus_gcomp_zero_solution_right * hgcrt_mod_right_gcrt_gcomp_zero_solution_right_congruence)) -> y = x

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

32 script commands · 8 reading checkpoints · 1 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 hlcm
  10. L10
    intro hzero
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hx
  2. L12
    intro hy
03Establish hmodL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt prefix solutions congruent lcm.

  1. L13
    have hmod : exists hgcrt_mod_left_gcrt_gcomp_zero_mod_actual hgcrt_mod_right_gcrt_gcomp_zero_mod_actual. y + M * hgcrt_mod_left_gcrt_gcomp_zero_mod_actual = x + M * hgcrt_mod_right_gcrt_gcomp_zero_mod_actual
  2. L14
    specialize crt_prefix_solutions_congruent_lcm r
  3. L15
    specialize crt_prefix_solutions_congruent_lcm s
  4. L16
    specialize crt_prefix_solutions_congruent_lcm b
  5. L17
    specialize crt_prefix_solutions_congruent_lcm c
  6. L18
    specialize crt_prefix_solutions_congruent_lcm l
  7. L19
    specialize crt_prefix_solutions_congruent_lcm M
  8. L20
    specialize crt_prefix_solutions_congruent_lcm y
  9. L21
    specialize crt_prefix_solutions_congruent_lcm x
  10. L22
    apply crt_prefix_solutions_congruent_lcm
04Use earlier factsL23–25

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

  1. L23
    exact hlcm
  2. L24
    exact hy
  3. L25
    exact hx
05Calculate and transport equalitiesL26–27

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L26
    rewrite hzero at hmod
  2. L27
    rewrite hzero at hmod
06Use earlier factsL28–29

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

  1. L28
    specialize mod_eq_zero_iff_eq y
  2. L29
    specialize mod_eq_zero_iff_eq x
07Separate the logical casesL30–30

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

  1. L30
    cases mod_eq_zero_iff_eq
08Use earlier factsL31–32

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

  1. L31
    apply mod_eq_zero_iff_eq_left
  2. L32
    exact hmod

Library-wide reading audit

Original defined command ledger · 32 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 hlcm
  10. 0010intro hzero
  11. 0011intro hx
  12. 0012intro hy
  13. 0013have hmod : exists hgcrt_mod_left_gcrt_gcomp_zero_mod_actual hgcrt_mod_right_gcrt_gcomp_zero_mod_actual. y + M * hgcrt_mod_left_gcrt_gcomp_zero_mod_actual = x + M * hgcrt_mod_right_gcrt_gcomp_zero_mod_actual
  14. 0014specialize crt_prefix_solutions_congruent_lcm r
  15. 0015specialize crt_prefix_solutions_congruent_lcm s
  16. 0016specialize crt_prefix_solutions_congruent_lcm b
  17. 0017specialize crt_prefix_solutions_congruent_lcm c
  18. 0018specialize crt_prefix_solutions_congruent_lcm l
  19. 0019specialize crt_prefix_solutions_congruent_lcm M
  20. 0020specialize crt_prefix_solutions_congruent_lcm y
  21. 0021specialize crt_prefix_solutions_congruent_lcm x
  22. 0022apply crt_prefix_solutions_congruent_lcm
  23. 0023exact hlcm
  24. 0024exact hy
  25. 0025exact hx
  26. 0026rewrite hzero at hmod
  27. 0027rewrite hzero at hmod
  28. 0028specialize mod_eq_zero_iff_eq y
  29. 0029specialize mod_eq_zero_iff_eq x
  30. 0030cases mod_eq_zero_iff_eq
  31. 0031apply mod_eq_zero_iff_eq_left
  32. 0032exact hmod