Pairwise gcd compatibility · arbitrary noncoprime lists · zero moduli

Complete finite generalized Chinese remainder theorem

Construct a simultaneous solution for every finite pairwise-compatible list, prove the exact LCM solution class, and obtain unique normalized representatives without a supplied compatible prefix or dominating last modulus.

24 kernel- and Lean-verified Alpha-closed theorems · 13 conservative definitions · 20 notation dependencies

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.

37 items
FC0001 crt_gcd_zero_right_value

A relational gcd with zero on the right equals its other input.

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

A gcd of a nonzero left input is nonzero, without restricting the right input.

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

A gcd of a nonzero right input is nonzero, including a zero left input.

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

A nonzero gcd yields both exact natural cofactors and their constructive coprimality.

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

Factoring a common gcd scale reduces unrestricted gcd--LCM distributivity to genuinely coprime cofactors.

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

GCD distributes over the actual binary LCM for a nonzero left input and nonzero comparison input; the right input may be zero.

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

The zero-left-modulus boundary of gcd--LCM distributivity follows from exact divisibility, not a positivity assumption.

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

Comparison with zero turns all three gcds into their other inputs and preserves the exact original LCM.

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

Unconditional constructive gcd(lcm(a,b),n)=lcm(gcd(a,n),gcd(b,n)), including every zero boundary.

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

Pointwise congruence modulo decoded gcds restricts to the preceding finite prefix.

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

Induction over every finite decoded modulus list lifts pointwise gcd congruences to congruence modulo the gcd of its exact list LCM; zero moduli and the empty list are included.

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

Pairwise compatibility and an actual prefix solution imply every gcd congruence needed for the next merge, without any dominating-last or coprimality assumption.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable
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
FC000F crt_pairwise_compatible_prefix_canonical_exists_unique

Full constructive canonical generalized CRT for arbitrary finite pairwise-compatible positive moduli: an exact list LCM and a unique strictly bounded simultaneous solution, with no supplied merge invariant or dominating modulus.

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

Every historical strictly bounded canonical solution is also a zero-safe normalized solution, without changing either definition.

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

Normalized representatives are literally unique at every list LCM; the zero case uses congruence equality, not a false bound below zero.

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

Every simultaneous solution has a normalized representative for its exact list LCM, with zero retained rather than divided by.

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

Full zero-inclusive generalized CRT: every arbitrary pairwise-compatible finite list has its exact LCM and a unique normalized simultaneous solution; neither positivity nor an operational merge invariant is assumed.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable
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
FC0015 crt_pairwise_compatible_prefix_merge_iff

Pairwise compatibility and the formerly stronger predecessor-LCM merge invariant are constructively equivalent for arbitrary finite natural lists.

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

All simultaneous solutions form exactly the congruence class of the normalized solution modulo the exact list LCM, also when that LCM is zero.

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

At zero list LCM every actual simultaneous solution equals the normalized one; no bound or normalization premise is imposed on the comparison solution.

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

For positive modulus lists, zero-safe normalization is exactly the historical strict canonical definition, not a weaker replacement.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable
PD0013 BetaAt(b,c,i,x)

x is the bounded beta-decoded value at index i.

Conservative definition · notation layer 0
PD0002 Lt(a,b)

Witness-defined strict order on natural numbers.

Conservative definition · notation layer 0
PD0003 Dvd(d,n)

The natural number d divides n.

Conservative definition · notation layer 0
PD0006 IsGCD(g,a,b)

g is a common divisor divisible by every common divisor.

Conservative definition · notation layer 1
PD0008 ModEq(m,a,b)

Balanced-natural congruence modulo m.

Conservative definition · notation layer 0
ND0001 Beta(b,c,i,x)

Exact hygienic Gödel-beta extraction; a signature-identical alias of checked BetaAt.

Conservative definition · notation layer 0
ND0056 CRTPrefixLCM(b,c,l,M)

The exact beta-prefix least common multiple, specified by divisibility and its universal leastness property.

Conservative definition · notation layer 1
ND0077 CRTNormalizedPrefixSolution(r,s,b,c,l,x,M)

The exact prefix LCM and an actual simultaneous solution, with x<M when M is positive; the zero-LCM case retains exact congruences rather than an impossible bound.

Conservative definition · notation layer 2
PD0001 Le(a,b)

Witness-defined non-strict order on natural numbers.

Conservative definition · notation layer 0

Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.