GC0005

crt_prefix_solution_implies_pairwise_compatible

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

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

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

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

crt_common_solution_implies_gcd_compatible Stable theorem; checked-use authorized

Direct dependents

GC0016 crt_merge_compatible_prefix_implies_pairwise_compatible

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

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.

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

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