Noncoprime constructive CRT compatibility and canonical solutions — Exact Proof Explorer

Every pair of natural residues is constructively congruent modulo one.

Any divisors of two coprime naturals are themselves constructively coprime.

The empty actual residue/modulus list is pairwise gcd-compatible.

Pairwise gcd compatibility of any finite list restricts to its predecessor prefix.

Every actual simultaneous solution forces exact pairwise gcd compatibility, including zero and non-coprime moduli.

The last residue of a compatible successor list is gcd-compatible with each earlier actual decoded pair.

The exact operational generalized-CRT merge invariant restricts to any predecessor prefix.

Exact gcd compatibility merges two arbitrary natural moduli, including zero, without any coprimality assumption.

Every arbitrary finite list, including non-coprime and zero moduli, has a genuine simultaneous solution whenever each exact predecessor-LCM merge is gcd-compatible.

The exact universal-property LCM of every finite positive modulus prefix is nonzero, including the empty prefix.

At list LCM zero, every simultaneous solution of an arbitrary decoded congruence system is literally unique.

Every arbitrary finite positive non-coprime congruence system satisfying the exact operational gcd-merge invariant has its genuine LCM and exactly one strictly bounded solution.

Multiplying a subtraction-free balanced Bezout equation preserves all four witnessed natural coefficients.

Every common natural scale, including zero, transports the full relational greatest-common-divisor specification constructively.

A multiplier coprime to the fixed right input does not change the full relational gcd of the left input.

Every natural product has an explicit first-order value witness without adding multiplication as a new operation.

For coprime natural factors and any nonzero comparison input, the gcd of their product is exactly the product of their individual relational gcd values.

For a nonzero relational gcd, the actual binary LCM is exactly its gcd times the product of the two coprime cofactors.

After factoring a common divisor from a multiplier and comparison input, the gcd is exactly that divisor times the gcd of the remaining coprime component.

A divisibility relation between inputs transports monotonically to their relational gcd values with any fixed natural, including zero.

GCD genuinely distributes over binary LCM whenever one modulus divides the other, including arbitrary zero inputs.

The operational predecessor-LCM merge invariant constructively implies exact pairwise gcd compatibility; the converse is not assumed.

Whenever the last modulus is an actual common multiple of all predecessors, exact pairwise gcd compatibility makes the last residue itself a simultaneous solution, including zero and non-coprime moduli.

Every positive pairwise gcd-compatible successor list whose last modulus dominates all predecessors has its exact list LCM and a unique strictly bounded simultaneous solution without assuming pairwise coprimality or the stronger merge invariant.