GC0005

crt_prefix_solution_implies_pairwise_compatible

Every actual simultaneous solution forces exact pairwise gcd compatibility, including zero and non-coprime moduli.

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. ∀ x. CRTPrefixSolution(r,s,b,c,l,x) → CRTPairwiseCompatiblePrefix(r,s,b,c,l)

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

Definition DAG

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

Actual proof prerequisites

crt_common_solution_implies_gcd_compatible · checked external prerequisite
Original expanded first-order statement 
forall r s b c l x. (forall gcrt_solution_index_gcomp_necessity_solution gcrt_solution_residue_gcomp_necessity_solution gcrt_solution_modulus_gcomp_necessity_solution. (exists ff_lt_gcrt_gcomp_necessity_solution_bound. ff_lt_gcrt_gcomp_necessity_solution_bound + S gcrt_solution_index_gcomp_necessity_solution = l) -> (((exists ff_h_gcrt_gcomp_necessity_solution_residue. ff_h_gcrt_gcomp_necessity_solution_residue + S (gcrt_solution_residue_gcomp_necessity_solution) = S ((S (gcrt_solution_index_gcomp_necessity_solution)) * s)) /\ exists ff_q_gcrt_gcomp_necessity_solution_residue. r = ff_q_gcrt_gcomp_necessity_solution_residue * S ((S (gcrt_solution_index_gcomp_necessity_solution)) * s) + (gcrt_solution_residue_gcomp_necessity_solution))) -> (((exists ff_h_gcrt_gcomp_necessity_solution_modulus. ff_h_gcrt_gcomp_necessity_solution_modulus + S (gcrt_solution_modulus_gcomp_necessity_solution) = S ((S (gcrt_solution_index_gcomp_necessity_solution)) * c)) /\ exists ff_q_gcrt_gcomp_necessity_solution_modulus. b = ff_q_gcrt_gcomp_necessity_solution_modulus * S ((S (gcrt_solution_index_gcomp_necessity_solution)) * c) + (gcrt_solution_modulus_gcomp_necessity_solution))) -> (exists hgcrt_mod_left_gcrt_gcomp_necessity_solution_congruence hgcrt_mod_right_gcrt_gcomp_necessity_solution_congruence. x + gcrt_solution_modulus_gcomp_necessity_solution * hgcrt_mod_left_gcrt_gcomp_necessity_solution_congruence = gcrt_solution_residue_gcomp_necessity_solution + gcrt_solution_modulus_gcomp_necessity_solution * hgcrt_mod_right_gcrt_gcomp_necessity_solution_congruence)) -> (forall gcomp_left_index_gcomp_necessity_pairs gcomp_right_index_gcomp_necessity_pairs gcomp_left_residue_gcomp_necessity_pairs gcomp_right_residue_gcomp_necessity_pairs gcomp_left_modulus_gcomp_necessity_pairs gcomp_right_modulus_gcomp_necessity_pairs gcomp_pair_gcd_gcomp_necessity_pairs. (exists ff_lt_gcrt_gcomp_necessity_pairs_left_bound. ff_lt_gcrt_gcomp_necessity_pairs_left_bound + S gcomp_left_index_gcomp_necessity_pairs = l) -> (exists ff_lt_gcrt_gcomp_necessity_pairs_right_bound. ff_lt_gcrt_gcomp_necessity_pairs_right_bound + S gcomp_right_index_gcomp_necessity_pairs = l) -> (((exists ff_h_gcrt_gcomp_necessity_pairs_left_residue. ff_h_gcrt_gcomp_necessity_pairs_left_residue + S (gcomp_left_residue_gcomp_necessity_pairs) = S ((S (gcomp_left_index_gcomp_necessity_pairs)) * s)) /\ exists ff_q_gcrt_gcomp_necessity_pairs_left_residue. r = ff_q_gcrt_gcomp_necessity_pairs_left_residue * S ((S (gcomp_left_index_gcomp_necessity_pairs)) * s) + (gcomp_left_residue_gcomp_necessity_pairs))) -> (((exists ff_h_gcrt_gcomp_necessity_pairs_right_residue. ff_h_gcrt_gcomp_necessity_pairs_right_residue + S (gcomp_right_residue_gcomp_necessity_pairs) = S ((S (gcomp_right_index_gcomp_necessity_pairs)) * s)) /\ exists ff_q_gcrt_gcomp_necessity_pairs_right_residue. r = ff_q_gcrt_gcomp_necessity_pairs_right_residue * S ((S (gcomp_right_index_gcomp_necessity_pairs)) * s) + (gcomp_right_residue_gcomp_necessity_pairs))) -> (((exists ff_h_gcrt_gcomp_necessity_pairs_left_modulus. ff_h_gcrt_gcomp_necessity_pairs_left_modulus + S (gcomp_left_modulus_gcomp_necessity_pairs) = S ((S (gcomp_left_index_gcomp_necessity_pairs)) * c)) /\ exists ff_q_gcrt_gcomp_necessity_pairs_left_modulus. b = ff_q_gcrt_gcomp_necessity_pairs_left_modulus * S ((S (gcomp_left_index_gcomp_necessity_pairs)) * c) + (gcomp_left_modulus_gcomp_necessity_pairs))) -> (((exists ff_h_gcrt_gcomp_necessity_pairs_right_modulus. ff_h_gcrt_gcomp_necessity_pairs_right_modulus + S (gcomp_right_modulus_gcomp_necessity_pairs) = S ((S (gcomp_right_index_gcomp_necessity_pairs)) * c)) /\ exists ff_q_gcrt_gcomp_necessity_pairs_right_modulus. b = ff_q_gcrt_gcomp_necessity_pairs_right_modulus * S ((S (gcomp_right_index_gcomp_necessity_pairs)) * c) + (gcomp_right_modulus_gcomp_necessity_pairs))) -> ((((exists hag_left_factor_gcomp_gcomp_necessity_pairs_gcd. gcomp_left_modulus_gcomp_necessity_pairs = gcomp_pair_gcd_gcomp_necessity_pairs * hag_left_factor_gcomp_gcomp_necessity_pairs_gcd) /\ (exists hag_right_factor_gcomp_gcomp_necessity_pairs_gcd. gcomp_right_modulus_gcomp_necessity_pairs = gcomp_pair_gcd_gcomp_necessity_pairs * hag_right_factor_gcomp_gcomp_necessity_pairs_gcd)) /\ forall hag_divisor_gcomp_gcomp_necessity_pairs_gcd. (exists hag_common_left_gcomp_gcomp_necessity_pairs_gcd. gcomp_left_modulus_gcomp_necessity_pairs = hag_divisor_gcomp_gcomp_necessity_pairs_gcd * hag_common_left_gcomp_gcomp_necessity_pairs_gcd) -> (exists hag_common_right_gcomp_gcomp_necessity_pairs_gcd. gcomp_right_modulus_gcomp_necessity_pairs = hag_divisor_gcomp_gcomp_necessity_pairs_gcd * hag_common_right_gcomp_gcomp_necessity_pairs_gcd) -> exists hag_greatest_factor_gcomp_gcomp_necessity_pairs_gcd. gcomp_pair_gcd_gcomp_necessity_pairs = hag_divisor_gcomp_gcomp_necessity_pairs_gcd * hag_greatest_factor_gcomp_gcomp_necessity_pairs_gcd)) -> (exists hgcrt_mod_left_gcrt_gcomp_necessity_pairs_result hgcrt_mod_right_gcrt_gcomp_necessity_pairs_result. gcomp_left_residue_gcomp_necessity_pairs + gcomp_pair_gcd_gcomp_necessity_pairs * hgcrt_mod_left_gcrt_gcomp_necessity_pairs_result = gcomp_right_residue_gcomp_necessity_pairs + gcomp_pair_gcd_gcomp_necessity_pairs * hgcrt_mod_right_gcrt_gcomp_necessity_pairs_result))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

44 script commands · 7 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 x
  7. L7
    intro hsolution
  8. L8
    intro i
  9. L9
    intro j
  10. L10
    intro a
02Fix variables and assumptionsL11–20

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

  1. L11
    intro d
  2. L12
    intro m
  3. L13
    intro n
  4. L14
    intro g
  5. L15
    intro hi
  6. L16
    intro hj
  7. L17
    intro ha
  8. L18
    intro hd
  9. L19
    intro hm
  10. L20
    intro hn
03Fix variables and assumptionsL21–21

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

  1. L21
    intro hg
04Use earlier factsL22–29

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

  1. L22
    specialize crt_common_solution_implies_gcd_compatible g
  2. L23
    specialize crt_common_solution_implies_gcd_compatible m
  3. L24
    specialize crt_common_solution_implies_gcd_compatible n
  4. L25
    specialize crt_common_solution_implies_gcd_compatible a
  5. L26
    specialize crt_common_solution_implies_gcd_compatible d
  6. L27
    specialize crt_common_solution_implies_gcd_compatible x
  7. L28
    apply crt_common_solution_implies_gcd_compatible
  8. L29
    exact hg
05Separate the logical casesL30–30

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

  1. L30
    split
06Use earlier factsL31–40

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

  1. L31
    specialize hsolution i
  2. L32
    specialize hsolution a
  3. L33
    specialize hsolution m
  4. L34
    apply hsolution
  5. L35
    exact hi
  6. L36
    exact ha
  7. L37
    exact hm
  8. L38
    specialize hsolution j
  9. L39
    specialize hsolution d
  10. L40
    specialize hsolution n
07Use earlier factsL41–44

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

  1. L41
    apply hsolution
  2. L42
    exact hj
  3. L43
    exact hd
  4. L44
    exact hn

Library-wide reading audit

Original defined command ledger · 44 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro x
  7. 0007intro hsolution
  8. 0008intro i
  9. 0009intro j
  10. 0010intro a
  11. 0011intro d
  12. 0012intro m
  13. 0013intro n
  14. 0014intro g
  15. 0015intro hi
  16. 0016intro hj
  17. 0017intro ha
  18. 0018intro hd
  19. 0019intro hm
  20. 0020intro hn
  21. 0021intro hg
  22. 0022specialize crt_common_solution_implies_gcd_compatible g
  23. 0023specialize crt_common_solution_implies_gcd_compatible m
  24. 0024specialize crt_common_solution_implies_gcd_compatible n
  25. 0025specialize crt_common_solution_implies_gcd_compatible a
  26. 0026specialize crt_common_solution_implies_gcd_compatible d
  27. 0027specialize crt_common_solution_implies_gcd_compatible x
  28. 0028apply crt_common_solution_implies_gcd_compatible
  29. 0029exact hg
  30. 0030split
  31. 0031specialize hsolution i
  32. 0032specialize hsolution a
  33. 0033specialize hsolution m
  34. 0034apply hsolution
  35. 0035exact hi
  36. 0036exact ha
  37. 0037exact hm
  38. 0038specialize hsolution j
  39. 0039specialize hsolution d
  40. 0040specialize hsolution n
  41. 0041apply hsolution
  42. 0042exact hj
  43. 0043exact hd
  44. 0044exact hn