Complete finite generalized Chinese remainder theorem — Exact Proof Explorer

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

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

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

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

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

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

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

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

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

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

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.

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

Every pairwise gcd-compatible finite list satisfies every actual predecessor-LCM merge condition, including arbitrary noncoprime and zero moduli.

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.

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.

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

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

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

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.

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

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

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

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

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