FC000E

crt_pairwise_compatible_prefix_solution_exists

Unrestricted finite-list generalized CRT: every pairwise-compatible decoded residue/modulus list has a genuine simultaneous natural solution, including zero and repeated moduli and empty lists.

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)

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_pairwise_compatible_prefix_implies_merge_compatiblecrt_merge_compatible_prefix_solution_exists · checked external prerequisite
Original expanded first-order statement 
forall r s b c l. (forall gcomp_left_index_gfull_full_existence_pairs gcomp_right_index_gfull_full_existence_pairs gcomp_left_residue_gfull_full_existence_pairs gcomp_right_residue_gfull_full_existence_pairs gcomp_left_modulus_gfull_full_existence_pairs gcomp_right_modulus_gfull_full_existence_pairs gcomp_pair_gcd_gfull_full_existence_pairs. (exists ff_lt_gcrt_gfull_full_existence_pairs_left_bound. ff_lt_gcrt_gfull_full_existence_pairs_left_bound + S gcomp_left_index_gfull_full_existence_pairs = l) -> (exists ff_lt_gcrt_gfull_full_existence_pairs_right_bound. ff_lt_gcrt_gfull_full_existence_pairs_right_bound + S gcomp_right_index_gfull_full_existence_pairs = l) -> (((exists ff_h_gcrt_gfull_full_existence_pairs_left_residue. ff_h_gcrt_gfull_full_existence_pairs_left_residue + S (gcomp_left_residue_gfull_full_existence_pairs) = S ((S (gcomp_left_index_gfull_full_existence_pairs)) * s)) /\ exists ff_q_gcrt_gfull_full_existence_pairs_left_residue. r = ff_q_gcrt_gfull_full_existence_pairs_left_residue * S ((S (gcomp_left_index_gfull_full_existence_pairs)) * s) + (gcomp_left_residue_gfull_full_existence_pairs))) -> (((exists ff_h_gcrt_gfull_full_existence_pairs_right_residue. ff_h_gcrt_gfull_full_existence_pairs_right_residue + S (gcomp_right_residue_gfull_full_existence_pairs) = S ((S (gcomp_right_index_gfull_full_existence_pairs)) * s)) /\ exists ff_q_gcrt_gfull_full_existence_pairs_right_residue. r = ff_q_gcrt_gfull_full_existence_pairs_right_residue * S ((S (gcomp_right_index_gfull_full_existence_pairs)) * s) + (gcomp_right_residue_gfull_full_existence_pairs))) -> (((exists ff_h_gcrt_gfull_full_existence_pairs_left_modulus. ff_h_gcrt_gfull_full_existence_pairs_left_modulus + S (gcomp_left_modulus_gfull_full_existence_pairs) = S ((S (gcomp_left_index_gfull_full_existence_pairs)) * c)) /\ exists ff_q_gcrt_gfull_full_existence_pairs_left_modulus. b = ff_q_gcrt_gfull_full_existence_pairs_left_modulus * S ((S (gcomp_left_index_gfull_full_existence_pairs)) * c) + (gcomp_left_modulus_gfull_full_existence_pairs))) -> (((exists ff_h_gcrt_gfull_full_existence_pairs_right_modulus. ff_h_gcrt_gfull_full_existence_pairs_right_modulus + S (gcomp_right_modulus_gfull_full_existence_pairs) = S ((S (gcomp_right_index_gfull_full_existence_pairs)) * c)) /\ exists ff_q_gcrt_gfull_full_existence_pairs_right_modulus. b = ff_q_gcrt_gfull_full_existence_pairs_right_modulus * S ((S (gcomp_right_index_gfull_full_existence_pairs)) * c) + (gcomp_right_modulus_gfull_full_existence_pairs))) -> ((((exists hag_left_factor_gcomp_gfull_full_existence_pairs_gcd. gcomp_left_modulus_gfull_full_existence_pairs = gcomp_pair_gcd_gfull_full_existence_pairs * hag_left_factor_gcomp_gfull_full_existence_pairs_gcd) /\ (exists hag_right_factor_gcomp_gfull_full_existence_pairs_gcd. gcomp_right_modulus_gfull_full_existence_pairs = gcomp_pair_gcd_gfull_full_existence_pairs * hag_right_factor_gcomp_gfull_full_existence_pairs_gcd)) /\ forall hag_divisor_gcomp_gfull_full_existence_pairs_gcd. (exists hag_common_left_gcomp_gfull_full_existence_pairs_gcd. gcomp_left_modulus_gfull_full_existence_pairs = hag_divisor_gcomp_gfull_full_existence_pairs_gcd * hag_common_left_gcomp_gfull_full_existence_pairs_gcd) -> (exists hag_common_right_gcomp_gfull_full_existence_pairs_gcd. gcomp_right_modulus_gfull_full_existence_pairs = hag_divisor_gcomp_gfull_full_existence_pairs_gcd * hag_common_right_gcomp_gfull_full_existence_pairs_gcd) -> exists hag_greatest_factor_gcomp_gfull_full_existence_pairs_gcd. gcomp_pair_gcd_gfull_full_existence_pairs = hag_divisor_gcomp_gfull_full_existence_pairs_gcd * hag_greatest_factor_gcomp_gfull_full_existence_pairs_gcd)) -> (exists hgcrt_mod_left_gcrt_gfull_full_existence_pairs_result hgcrt_mod_right_gcrt_gfull_full_existence_pairs_result. gcomp_left_residue_gfull_full_existence_pairs + gcomp_pair_gcd_gfull_full_existence_pairs * hgcrt_mod_left_gcrt_gfull_full_existence_pairs_result = gcomp_right_residue_gfull_full_existence_pairs + gcomp_pair_gcd_gfull_full_existence_pairs * hgcrt_mod_right_gcrt_gfull_full_existence_pairs_result)) -> exists x. (forall gcrt_solution_index_gfull_full_existence_solution gcrt_solution_residue_gfull_full_existence_solution gcrt_solution_modulus_gfull_full_existence_solution. (exists ff_lt_gcrt_gfull_full_existence_solution_bound. ff_lt_gcrt_gfull_full_existence_solution_bound + S gcrt_solution_index_gfull_full_existence_solution = l) -> (((exists ff_h_gcrt_gfull_full_existence_solution_residue. ff_h_gcrt_gfull_full_existence_solution_residue + S (gcrt_solution_residue_gfull_full_existence_solution) = S ((S (gcrt_solution_index_gfull_full_existence_solution)) * s)) /\ exists ff_q_gcrt_gfull_full_existence_solution_residue. r = ff_q_gcrt_gfull_full_existence_solution_residue * S ((S (gcrt_solution_index_gfull_full_existence_solution)) * s) + (gcrt_solution_residue_gfull_full_existence_solution))) -> (((exists ff_h_gcrt_gfull_full_existence_solution_modulus. ff_h_gcrt_gfull_full_existence_solution_modulus + S (gcrt_solution_modulus_gfull_full_existence_solution) = S ((S (gcrt_solution_index_gfull_full_existence_solution)) * c)) /\ exists ff_q_gcrt_gfull_full_existence_solution_modulus. b = ff_q_gcrt_gfull_full_existence_solution_modulus * S ((S (gcrt_solution_index_gfull_full_existence_solution)) * c) + (gcrt_solution_modulus_gfull_full_existence_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_full_existence_solution_congruence hgcrt_mod_right_gcrt_gfull_full_existence_solution_congruence. x + gcrt_solution_modulus_gfull_full_existence_solution * hgcrt_mod_left_gcrt_gfull_full_existence_solution_congruence = gcrt_solution_residue_gfull_full_existence_solution + gcrt_solution_modulus_gfull_full_existence_solution * hgcrt_mod_right_gcrt_gfull_full_existence_solution_congruence))

Complete tactic proof in conservative notation

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

19 script commands · 3 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 implies merge compatible
01Fix variables and assumptionsL1–6

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 hp
02Use earlier factsL7–16

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

  1. L7
    specialize crt_merge_compatible_prefix_solution_exists r
  2. L8
    specialize crt_merge_compatible_prefix_solution_exists s
  3. L9
    specialize crt_merge_compatible_prefix_solution_exists b
  4. L10
    specialize crt_merge_compatible_prefix_solution_exists c
  5. L11
    specialize crt_merge_compatible_prefix_solution_exists l
  6. L12
    apply crt_merge_compatible_prefix_solution_exists
  7. L13
    specialize crt_pairwise_compatible_prefix_implies_merge_compatible r
  8. L14
    specialize crt_pairwise_compatible_prefix_implies_merge_compatible s
  9. L15
    specialize crt_pairwise_compatible_prefix_implies_merge_compatible b
  10. L16
    specialize crt_pairwise_compatible_prefix_implies_merge_compatible c
03Use earlier factsL17–19

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

  1. L17
    specialize crt_pairwise_compatible_prefix_implies_merge_compatible l
  2. L18
    apply crt_pairwise_compatible_prefix_implies_merge_compatible
  3. L19
    exact hp

Library-wide reading audit

Original defined command ledger · 19 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro hp
  7. 0007specialize crt_merge_compatible_prefix_solution_exists r
  8. 0008specialize crt_merge_compatible_prefix_solution_exists s
  9. 0009specialize crt_merge_compatible_prefix_solution_exists b
  10. 0010specialize crt_merge_compatible_prefix_solution_exists c
  11. 0011specialize crt_merge_compatible_prefix_solution_exists l
  12. 0012apply crt_merge_compatible_prefix_solution_exists
  13. 0013specialize crt_pairwise_compatible_prefix_implies_merge_compatible r
  14. 0014specialize crt_pairwise_compatible_prefix_implies_merge_compatible s
  15. 0015specialize crt_pairwise_compatible_prefix_implies_merge_compatible b
  16. 0016specialize crt_pairwise_compatible_prefix_implies_merge_compatible c
  17. 0017specialize crt_pairwise_compatible_prefix_implies_merge_compatible l
  18. 0018apply crt_pairwise_compatible_prefix_implies_merge_compatible
  19. 0019exact hp