Finite Compatible CRT

Abstract

Finite congruences glue exactly under pairwise gcd compatibility, uniquely modulo lcm.

Theorem 1.1 (Finite CRT gluing and integer representatives).

$$\forall I:Type,[\mathrm{Fintype}(I)],m:I\to \mathbb{N},a:I\to \mathbb{Z},((\forall i:I,\forall j:I,i\ne j\Rightarrow \mathrm{Coprime}(m(i),m(j)))\Rightarrow \exists !z:\mathrm{ZMod}(\prod _{i\in I}m(i)),\forall i:I,\mathrm{pi}(i,z)=a(i))\wedge ((\forall i:I,\forall j:I,\mathrm{ModEq}(\gcd (m(i),m(j)),a(i),a(j)))⟺(\exists x:\mathbb{Z},\forall y:\mathbb{Z},((\forall i:I,\mathrm{ModEq}(m(i),y,a(i)))⟺\mathrm{ModEq}({\mathrm{lcm}}_{i\in I}m(i),y,x))))\wedge ((\forall i:I,m(i)\ne 0)\Rightarrow \forall x:\mathbb{Z},\exists y:\mathbb{Z},y\ne x\wedge (\forall i:I,\mathrm{ModEq}(m(i),y,x))).$$

Proof. Machine-checked in Lean as D5/S3/Factorization/PrimePowers/FiniteCompatibleCrt.finite_crt_gluing (✓ std3). ∎

Source. Repository-derived.

Commentary.

The index type I is finite, m assigns natural moduli, and a assigns integer representatives of the local data. P is the product of all m(i), L is their finite least common multiple, and pi(i,z) is the canonical ZMod castHom from modulus P to modulus m(i). The right side a(i) of the first equality is cast into ZMod(m(i)).

ModEq(n,x,y) means integer congruence modulo n. The middle clause identifies the entire solution set with one congruence class modulo L; setting y=x also supplies a simultaneous solution. Empty index types are included, with P=L=1. Zero moduli are allowed in the first two clauses; ZMod(0) records the whole integer.

The last clause assumes nonzero natural moduli, hence positive moduli. Adding P gives a distinct integer with the same finite residue data. Selecting an ordinary integer therefore requires additional restrictions such as a suitable bounded interval; sign alone is not asserted to suffice.

The proof imports the frozen binary compatible-residue image theorem. Finite induction derives compatibility between a merged solution and the next residue across gcd(L,m(j)), using gcd distribution over finite lcm, and then applies binary gluing. The coprime clause uses pinned Mathlib’s ZMod.prodEquivPi.

References

• Truth anchor: D5/S3/Factorization/PrimePowers/FiniteCompatibleCrt.finite_crt_gluing
• Dependency: D5/S3/Factorization/PrimePowers/CompatibleResidueJointImage