FC0001 crt_gcd_zero_right_valueA relational gcd with zero on the right equals its other input.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StablePairwise gcd compatibility · arbitrary noncoprime lists · zero moduli
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.
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.
FC0001 crt_gcd_zero_right_valueA relational gcd with zero on the right equals its other input.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableFC0002 crt_gcd_nonzero_leftA 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 StableFC0003 crt_gcd_nonzero_rightA 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 StableFC0004 crt_gcd_coprime_cofactorsA nonzero gcd yields both exact natural cofactors and their constructive coprimality.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableFC0005 crt_gcd_lcm_distributes_scaled_coprimeFactoring 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 StableFC0006 crt_gcd_lcm_distributes_nonzeroGCD 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 StableFC0007 crt_gcd_lcm_distributes_zero_leftThe 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 StableFC0008 crt_gcd_lcm_distributes_zero_comparisonComparison 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 StableFC0009 crt_gcd_lcm_distributesUnconditional 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 StableFC000A crt_prefix_gcd_congruences_drop_lastPointwise congruence modulo decoded gcds restricts to the preceding finite prefix.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableFC000B crt_prefix_gcd_congruences_lcmInduction 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 StableFC000C crt_pairwise_compatible_prefix_induces_gcd_congruencesPairwise 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 StableFC000D crt_pairwise_compatible_prefix_implies_merge_compatibleEvery pairwise gcd-compatible finite list satisfies every actual predecessor-LCM merge condition, including arbitrary noncoprime and zero moduli.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableFC000E crt_pairwise_compatible_prefix_solution_existsUnrestricted 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 StableFC000F crt_pairwise_compatible_prefix_canonical_exists_uniqueFull 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 StableFC0010 crt_canonical_prefix_solution_implies_normalizedEvery 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 StableFC0011 crt_normalized_prefix_solution_uniqueNormalized 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 StableFC0012 crt_prefix_solution_normalized_existsEvery 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 StableFC0013 crt_pairwise_compatible_prefix_normalized_exists_uniqueFull 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 StableFC0014 crt_pairwise_compatible_prefix_solvable_iffExact 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 StableFC0015 crt_pairwise_compatible_prefix_merge_iffPairwise 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 StableFC0016 crt_normalized_prefix_solution_class_iff_lcmAll 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 StableFC0017 crt_normalized_zero_lcm_all_solutions_uniqueAt 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 StableFC0018 crt_positive_normalized_prefix_iff_canonicalFor 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 StablePD0013 BetaAt(b,c,i,x)x is the bounded beta-decoded value at index i.
Conservative definition · notation layer 0PD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0PD0003 Dvd(d,n)The natural number d divides n.
Conservative definition · notation layer 0PD0006 IsGCD(g,a,b)g is a common divisor divisible by every common divisor.
Conservative definition · notation layer 1PD0008 ModEq(m,a,b)Balanced-natural congruence modulo m.
Conservative definition · notation layer 0ND0076 CRTPrefixGcdCongruences(b,c,l,m,u,v)The two residues agree modulo the actual gcd of each decoded prefix modulus with m.
Conservative definition · notation layer 2ND0001 Beta(b,c,i,x)Exact hygienic Gödel-beta extraction; a signature-identical alias of checked BetaAt.
Conservative definition · notation layer 0ND0056 CRTPrefixLCM(b,c,l,M)The exact beta-prefix least common multiple, specified by divisibility and its universal leastness property.
Conservative definition · notation layer 1ND0055 CRTPrefixSolution(r,s,b,c,l,x)One actual simultaneous solution to every beta-coded finite residue/modulus pair.
Conservative definition · notation layer 1ND0077 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 2ND0067 CRTPairwiseCompatiblePrefix(r,s,b,c,l)Every pair of finite beta-coded residue/modulus entries agrees modulo its genuinely witnessed greatest common divisor.
Conservative definition · notation layer 2ND0053 CRTPositiveModuliPrefix(b,c,l)A bounded beta-coded finite prefix consisting entirely of genuinely positive moduli.
Conservative definition · notation layer 1PD0001 Le(a,b)Witness-defined non-strict order on natural numbers.
Conservative definition · notation layer 0Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.