FC000E

crt_pairwise_compatible_prefix_solution_exists

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

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.

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

Constructive proof overview

Generated structural guide

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.

The unchanged tactic script uses 2 declared prerequisites and contains 19 exact native proof lines.

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

Proof neighborhood

Direct dependencies

FC000D crt_pairwise_compatible_prefix_implies_merge_compatible crt_merge_compatible_prefix_solution_exists Alpha theorem; checked-use authorized

Direct dependents

FC0013 crt_pairwise_compatible_prefix_normalized_exists_unique FC0014 crt_pairwise_compatible_prefix_solvable_iff

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

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.

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