FC0014

crt_pairwise_compatible_prefix_solvable_iff

Exact pairwise gcd compatibility is necessary and sufficient for solvability of every finite natural congruence list, including zero moduli.

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

Actual proof prerequisites

crt_pairwise_compatible_prefix_solution_existscrt_prefix_solution_implies_pairwise_compatible · checked external prerequisite
Original expanded first-order statement 
forall r s b c l. (((forall gcomp_left_index_gfull_solvable_pairs_forward gcomp_right_index_gfull_solvable_pairs_forward gcomp_left_residue_gfull_solvable_pairs_forward gcomp_right_residue_gfull_solvable_pairs_forward gcomp_left_modulus_gfull_solvable_pairs_forward gcomp_right_modulus_gfull_solvable_pairs_forward gcomp_pair_gcd_gfull_solvable_pairs_forward. (exists ff_lt_gcrt_gfull_solvable_pairs_forward_left_bound. ff_lt_gcrt_gfull_solvable_pairs_forward_left_bound + S gcomp_left_index_gfull_solvable_pairs_forward = l) -> (exists ff_lt_gcrt_gfull_solvable_pairs_forward_right_bound. ff_lt_gcrt_gfull_solvable_pairs_forward_right_bound + S gcomp_right_index_gfull_solvable_pairs_forward = l) -> (((exists ff_h_gcrt_gfull_solvable_pairs_forward_left_residue. ff_h_gcrt_gfull_solvable_pairs_forward_left_residue + S (gcomp_left_residue_gfull_solvable_pairs_forward) = S ((S (gcomp_left_index_gfull_solvable_pairs_forward)) * s)) /\ exists ff_q_gcrt_gfull_solvable_pairs_forward_left_residue. r = ff_q_gcrt_gfull_solvable_pairs_forward_left_residue * S ((S (gcomp_left_index_gfull_solvable_pairs_forward)) * s) + (gcomp_left_residue_gfull_solvable_pairs_forward))) -> (((exists ff_h_gcrt_gfull_solvable_pairs_forward_right_residue. ff_h_gcrt_gfull_solvable_pairs_forward_right_residue + S (gcomp_right_residue_gfull_solvable_pairs_forward) = S ((S (gcomp_right_index_gfull_solvable_pairs_forward)) * s)) /\ exists ff_q_gcrt_gfull_solvable_pairs_forward_right_residue. r = ff_q_gcrt_gfull_solvable_pairs_forward_right_residue * S ((S (gcomp_right_index_gfull_solvable_pairs_forward)) * s) + (gcomp_right_residue_gfull_solvable_pairs_forward))) -> (((exists ff_h_gcrt_gfull_solvable_pairs_forward_left_modulus. ff_h_gcrt_gfull_solvable_pairs_forward_left_modulus + S (gcomp_left_modulus_gfull_solvable_pairs_forward) = S ((S (gcomp_left_index_gfull_solvable_pairs_forward)) * c)) /\ exists ff_q_gcrt_gfull_solvable_pairs_forward_left_modulus. b = ff_q_gcrt_gfull_solvable_pairs_forward_left_modulus * S ((S (gcomp_left_index_gfull_solvable_pairs_forward)) * c) + (gcomp_left_modulus_gfull_solvable_pairs_forward))) -> (((exists ff_h_gcrt_gfull_solvable_pairs_forward_right_modulus. ff_h_gcrt_gfull_solvable_pairs_forward_right_modulus + S (gcomp_right_modulus_gfull_solvable_pairs_forward) = S ((S (gcomp_right_index_gfull_solvable_pairs_forward)) * c)) /\ exists ff_q_gcrt_gfull_solvable_pairs_forward_right_modulus. b = ff_q_gcrt_gfull_solvable_pairs_forward_right_modulus * S ((S (gcomp_right_index_gfull_solvable_pairs_forward)) * c) + (gcomp_right_modulus_gfull_solvable_pairs_forward))) -> ((((exists hag_left_factor_gcomp_gfull_solvable_pairs_forward_gcd. gcomp_left_modulus_gfull_solvable_pairs_forward = gcomp_pair_gcd_gfull_solvable_pairs_forward * hag_left_factor_gcomp_gfull_solvable_pairs_forward_gcd) /\ (exists hag_right_factor_gcomp_gfull_solvable_pairs_forward_gcd. gcomp_right_modulus_gfull_solvable_pairs_forward = gcomp_pair_gcd_gfull_solvable_pairs_forward * hag_right_factor_gcomp_gfull_solvable_pairs_forward_gcd)) /\ forall hag_divisor_gcomp_gfull_solvable_pairs_forward_gcd. (exists hag_common_left_gcomp_gfull_solvable_pairs_forward_gcd. gcomp_left_modulus_gfull_solvable_pairs_forward = hag_divisor_gcomp_gfull_solvable_pairs_forward_gcd * hag_common_left_gcomp_gfull_solvable_pairs_forward_gcd) -> (exists hag_common_right_gcomp_gfull_solvable_pairs_forward_gcd. gcomp_right_modulus_gfull_solvable_pairs_forward = hag_divisor_gcomp_gfull_solvable_pairs_forward_gcd * hag_common_right_gcomp_gfull_solvable_pairs_forward_gcd) -> exists hag_greatest_factor_gcomp_gfull_solvable_pairs_forward_gcd. gcomp_pair_gcd_gfull_solvable_pairs_forward = hag_divisor_gcomp_gfull_solvable_pairs_forward_gcd * hag_greatest_factor_gcomp_gfull_solvable_pairs_forward_gcd)) -> (exists hgcrt_mod_left_gcrt_gfull_solvable_pairs_forward_result hgcrt_mod_right_gcrt_gfull_solvable_pairs_forward_result. gcomp_left_residue_gfull_solvable_pairs_forward + gcomp_pair_gcd_gfull_solvable_pairs_forward * hgcrt_mod_left_gcrt_gfull_solvable_pairs_forward_result = gcomp_right_residue_gfull_solvable_pairs_forward + gcomp_pair_gcd_gfull_solvable_pairs_forward * hgcrt_mod_right_gcrt_gfull_solvable_pairs_forward_result)) -> exists x. (forall gcrt_solution_index_gfull_solvable_solution_forward gcrt_solution_residue_gfull_solvable_solution_forward gcrt_solution_modulus_gfull_solvable_solution_forward. (exists ff_lt_gcrt_gfull_solvable_solution_forward_bound. ff_lt_gcrt_gfull_solvable_solution_forward_bound + S gcrt_solution_index_gfull_solvable_solution_forward = l) -> (((exists ff_h_gcrt_gfull_solvable_solution_forward_residue. ff_h_gcrt_gfull_solvable_solution_forward_residue + S (gcrt_solution_residue_gfull_solvable_solution_forward) = S ((S (gcrt_solution_index_gfull_solvable_solution_forward)) * s)) /\ exists ff_q_gcrt_gfull_solvable_solution_forward_residue. r = ff_q_gcrt_gfull_solvable_solution_forward_residue * S ((S (gcrt_solution_index_gfull_solvable_solution_forward)) * s) + (gcrt_solution_residue_gfull_solvable_solution_forward))) -> (((exists ff_h_gcrt_gfull_solvable_solution_forward_modulus. ff_h_gcrt_gfull_solvable_solution_forward_modulus + S (gcrt_solution_modulus_gfull_solvable_solution_forward) = S ((S (gcrt_solution_index_gfull_solvable_solution_forward)) * c)) /\ exists ff_q_gcrt_gfull_solvable_solution_forward_modulus. b = ff_q_gcrt_gfull_solvable_solution_forward_modulus * S ((S (gcrt_solution_index_gfull_solvable_solution_forward)) * c) + (gcrt_solution_modulus_gfull_solvable_solution_forward))) -> (exists hgcrt_mod_left_gcrt_gfull_solvable_solution_forward_congruence hgcrt_mod_right_gcrt_gfull_solvable_solution_forward_congruence. x + gcrt_solution_modulus_gfull_solvable_solution_forward * hgcrt_mod_left_gcrt_gfull_solvable_solution_forward_congruence = gcrt_solution_residue_gfull_solvable_solution_forward + gcrt_solution_modulus_gfull_solvable_solution_forward * hgcrt_mod_right_gcrt_gfull_solvable_solution_forward_congruence))) /\ ((exists x. (forall gcrt_solution_index_gfull_solvable_solution_backward gcrt_solution_residue_gfull_solvable_solution_backward gcrt_solution_modulus_gfull_solvable_solution_backward. (exists ff_lt_gcrt_gfull_solvable_solution_backward_bound. ff_lt_gcrt_gfull_solvable_solution_backward_bound + S gcrt_solution_index_gfull_solvable_solution_backward = l) -> (((exists ff_h_gcrt_gfull_solvable_solution_backward_residue. ff_h_gcrt_gfull_solvable_solution_backward_residue + S (gcrt_solution_residue_gfull_solvable_solution_backward) = S ((S (gcrt_solution_index_gfull_solvable_solution_backward)) * s)) /\ exists ff_q_gcrt_gfull_solvable_solution_backward_residue. r = ff_q_gcrt_gfull_solvable_solution_backward_residue * S ((S (gcrt_solution_index_gfull_solvable_solution_backward)) * s) + (gcrt_solution_residue_gfull_solvable_solution_backward))) -> (((exists ff_h_gcrt_gfull_solvable_solution_backward_modulus. ff_h_gcrt_gfull_solvable_solution_backward_modulus + S (gcrt_solution_modulus_gfull_solvable_solution_backward) = S ((S (gcrt_solution_index_gfull_solvable_solution_backward)) * c)) /\ exists ff_q_gcrt_gfull_solvable_solution_backward_modulus. b = ff_q_gcrt_gfull_solvable_solution_backward_modulus * S ((S (gcrt_solution_index_gfull_solvable_solution_backward)) * c) + (gcrt_solution_modulus_gfull_solvable_solution_backward))) -> (exists hgcrt_mod_left_gcrt_gfull_solvable_solution_backward_congruence hgcrt_mod_right_gcrt_gfull_solvable_solution_backward_congruence. x + gcrt_solution_modulus_gfull_solvable_solution_backward * hgcrt_mod_left_gcrt_gfull_solvable_solution_backward_congruence = gcrt_solution_residue_gfull_solvable_solution_backward + gcrt_solution_modulus_gfull_solvable_solution_backward * hgcrt_mod_right_gcrt_gfull_solvable_solution_backward_congruence))) -> (forall gcomp_left_index_gfull_solvable_pairs_backward gcomp_right_index_gfull_solvable_pairs_backward gcomp_left_residue_gfull_solvable_pairs_backward gcomp_right_residue_gfull_solvable_pairs_backward gcomp_left_modulus_gfull_solvable_pairs_backward gcomp_right_modulus_gfull_solvable_pairs_backward gcomp_pair_gcd_gfull_solvable_pairs_backward. (exists ff_lt_gcrt_gfull_solvable_pairs_backward_left_bound. ff_lt_gcrt_gfull_solvable_pairs_backward_left_bound + S gcomp_left_index_gfull_solvable_pairs_backward = l) -> (exists ff_lt_gcrt_gfull_solvable_pairs_backward_right_bound. ff_lt_gcrt_gfull_solvable_pairs_backward_right_bound + S gcomp_right_index_gfull_solvable_pairs_backward = l) -> (((exists ff_h_gcrt_gfull_solvable_pairs_backward_left_residue. ff_h_gcrt_gfull_solvable_pairs_backward_left_residue + S (gcomp_left_residue_gfull_solvable_pairs_backward) = S ((S (gcomp_left_index_gfull_solvable_pairs_backward)) * s)) /\ exists ff_q_gcrt_gfull_solvable_pairs_backward_left_residue. r = ff_q_gcrt_gfull_solvable_pairs_backward_left_residue * S ((S (gcomp_left_index_gfull_solvable_pairs_backward)) * s) + (gcomp_left_residue_gfull_solvable_pairs_backward))) -> (((exists ff_h_gcrt_gfull_solvable_pairs_backward_right_residue. ff_h_gcrt_gfull_solvable_pairs_backward_right_residue + S (gcomp_right_residue_gfull_solvable_pairs_backward) = S ((S (gcomp_right_index_gfull_solvable_pairs_backward)) * s)) /\ exists ff_q_gcrt_gfull_solvable_pairs_backward_right_residue. r = ff_q_gcrt_gfull_solvable_pairs_backward_right_residue * S ((S (gcomp_right_index_gfull_solvable_pairs_backward)) * s) + (gcomp_right_residue_gfull_solvable_pairs_backward))) -> (((exists ff_h_gcrt_gfull_solvable_pairs_backward_left_modulus. ff_h_gcrt_gfull_solvable_pairs_backward_left_modulus + S (gcomp_left_modulus_gfull_solvable_pairs_backward) = S ((S (gcomp_left_index_gfull_solvable_pairs_backward)) * c)) /\ exists ff_q_gcrt_gfull_solvable_pairs_backward_left_modulus. b = ff_q_gcrt_gfull_solvable_pairs_backward_left_modulus * S ((S (gcomp_left_index_gfull_solvable_pairs_backward)) * c) + (gcomp_left_modulus_gfull_solvable_pairs_backward))) -> (((exists ff_h_gcrt_gfull_solvable_pairs_backward_right_modulus. ff_h_gcrt_gfull_solvable_pairs_backward_right_modulus + S (gcomp_right_modulus_gfull_solvable_pairs_backward) = S ((S (gcomp_right_index_gfull_solvable_pairs_backward)) * c)) /\ exists ff_q_gcrt_gfull_solvable_pairs_backward_right_modulus. b = ff_q_gcrt_gfull_solvable_pairs_backward_right_modulus * S ((S (gcomp_right_index_gfull_solvable_pairs_backward)) * c) + (gcomp_right_modulus_gfull_solvable_pairs_backward))) -> ((((exists hag_left_factor_gcomp_gfull_solvable_pairs_backward_gcd. gcomp_left_modulus_gfull_solvable_pairs_backward = gcomp_pair_gcd_gfull_solvable_pairs_backward * hag_left_factor_gcomp_gfull_solvable_pairs_backward_gcd) /\ (exists hag_right_factor_gcomp_gfull_solvable_pairs_backward_gcd. gcomp_right_modulus_gfull_solvable_pairs_backward = gcomp_pair_gcd_gfull_solvable_pairs_backward * hag_right_factor_gcomp_gfull_solvable_pairs_backward_gcd)) /\ forall hag_divisor_gcomp_gfull_solvable_pairs_backward_gcd. (exists hag_common_left_gcomp_gfull_solvable_pairs_backward_gcd. gcomp_left_modulus_gfull_solvable_pairs_backward = hag_divisor_gcomp_gfull_solvable_pairs_backward_gcd * hag_common_left_gcomp_gfull_solvable_pairs_backward_gcd) -> (exists hag_common_right_gcomp_gfull_solvable_pairs_backward_gcd. gcomp_right_modulus_gfull_solvable_pairs_backward = hag_divisor_gcomp_gfull_solvable_pairs_backward_gcd * hag_common_right_gcomp_gfull_solvable_pairs_backward_gcd) -> exists hag_greatest_factor_gcomp_gfull_solvable_pairs_backward_gcd. gcomp_pair_gcd_gfull_solvable_pairs_backward = hag_divisor_gcomp_gfull_solvable_pairs_backward_gcd * hag_greatest_factor_gcomp_gfull_solvable_pairs_backward_gcd)) -> (exists hgcrt_mod_left_gcrt_gfull_solvable_pairs_backward_result hgcrt_mod_right_gcrt_gfull_solvable_pairs_backward_result. gcomp_left_residue_gfull_solvable_pairs_backward + gcomp_pair_gcd_gfull_solvable_pairs_backward * hgcrt_mod_left_gcrt_gfull_solvable_pairs_backward_result = gcomp_right_residue_gfull_solvable_pairs_backward + gcomp_pair_gcd_gfull_solvable_pairs_backward * hgcrt_mod_right_gcrt_gfull_solvable_pairs_backward_result))))

Complete tactic proof in conservative notation

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

24 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.

Named ingredients (1)
crt pairwise compatible prefix solution exists
01Fix variables and assumptionsL1–5

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
02Separate the logical casesL6–6

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

  1. L6
    split
03Fix variables and assumptionsL7–7

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

  1. L7
    intro hp
04Use earlier factsL8–14

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

  1. L8
    specialize crt_pairwise_compatible_prefix_solution_exists r
  2. L9
    specialize crt_pairwise_compatible_prefix_solution_exists s
  3. L10
    specialize crt_pairwise_compatible_prefix_solution_exists b
  4. L11
    specialize crt_pairwise_compatible_prefix_solution_exists c
  5. L12
    specialize crt_pairwise_compatible_prefix_solution_exists l
  6. L13
    apply crt_pairwise_compatible_prefix_solution_exists
  7. L14
    exact hp
05Fix variables and assumptionsL15–15

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

  1. L15
    intro hs
06Separate the logical casesL16–16

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

  1. L16
    cases hs
07Use earlier factsL17–24

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

  1. L17
    specialize crt_prefix_solution_implies_pairwise_compatible r
  2. L18
    specialize crt_prefix_solution_implies_pairwise_compatible s
  3. L19
    specialize crt_prefix_solution_implies_pairwise_compatible b
  4. L20
    specialize crt_prefix_solution_implies_pairwise_compatible c
  5. L21
    specialize crt_prefix_solution_implies_pairwise_compatible l
  6. L22
    specialize crt_prefix_solution_implies_pairwise_compatible x
  7. L23
    apply crt_prefix_solution_implies_pairwise_compatible
  8. L24
    exact hs_witness

Library-wide reading audit

Original defined command ledger · 24 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006split
  7. 0007intro hp
  8. 0008specialize crt_pairwise_compatible_prefix_solution_exists r
  9. 0009specialize crt_pairwise_compatible_prefix_solution_exists s
  10. 0010specialize crt_pairwise_compatible_prefix_solution_exists b
  11. 0011specialize crt_pairwise_compatible_prefix_solution_exists c
  12. 0012specialize crt_pairwise_compatible_prefix_solution_exists l
  13. 0013apply crt_pairwise_compatible_prefix_solution_exists
  14. 0014exact hp
  15. 0015intro hs
  16. 0016cases hs
  17. 0017specialize crt_prefix_solution_implies_pairwise_compatible r
  18. 0018specialize crt_prefix_solution_implies_pairwise_compatible s
  19. 0019specialize crt_prefix_solution_implies_pairwise_compatible b
  20. 0020specialize crt_prefix_solution_implies_pairwise_compatible c
  21. 0021specialize crt_prefix_solution_implies_pairwise_compatible l
  22. 0022specialize crt_prefix_solution_implies_pairwise_compatible x
  23. 0023apply crt_prefix_solution_implies_pairwise_compatible
  24. 0024exact hs_witness