Finite Chinese remainder theorem and canonical LCM solutions — Exact Proof Explorer

An empty decoded modulus prefix has no zero-valued member.

Positivity of a successor-length modulus list restricts to its predecessor prefix.

The final decoded modulus of a positive successor list is nonzero.

Pairwise coprimality of decoded moduli restricts to every predecessor prefix.

Every natural number solves the empty simultaneous-congruence system.

A solution of a successor list remains a solution of the predecessor prefix.

The last residue/modulus pair of a solved successor list satisfies its actual congruence.

A solved predecessor prefix extends exactly when the actual last decoded congruence holds.

The last decoded modulus is coprime to every actual earlier modulus in a pairwise-coprime list.

A genuine beta-coded product of an arbitrary positive finite modulus list is nonzero.

The actual finite beta-product is a common multiple of every decoded modulus.

For pairwise-coprime decoded moduli the actual finite product is exactly their universal-property lcm.

The universal-property lcm of any decoded finite modulus prefix is unique whenever it exists.

The universal-property lcm of the empty decoded modulus list is exactly one.

Binary relational lcm extends the exact universal-property lcm of any finite decoded modulus prefix.

Every arbitrary finite decoded modulus list, including noncoprime and zero entries, has a unique exact lcm.

Every arbitrary finite pairwise-coprime modulus list has a unique relational lcm.

The actual predecessor product is coprime to the final modulus of any pairwise-coprime list.

Every arbitrary finite beta-coded list of positive pairwise-coprime moduli has an actual simultaneous CRT solution.

Two simultaneous solutions are congruent modulo every actually decoded list modulus.

Congruence modulo any common multiple transports an actual simultaneous-list solution.

For every finite list, the directed gap between two solutions is divisible by its universal-property lcm.

For arbitrary decoded lists, every two simultaneous solutions are congruent modulo the exact list lcm.

The complete solution class of any finite system is exactly one congruence class modulo its list lcm.

Every existing finite-list solution has an actual canonical representative strictly below its nonzero list lcm.

The strictly bounded canonical representative of any finite decoded CRT system is unique.

Every arbitrary finite list of positive pairwise-coprime moduli has its exact lcm and a unique actual bounded CRT solution.