Finite-Window CRT Indistinguishability

Abstract

Every finite coprime residue window is realized by a natural-number shift, with an explicit three-modulus certificate.

Theorem 1.1 (A finite coprime window cannot separate a shift).

$$\forall W:\mathrm{Finset}\left(\mathbb{N}\right),(\forall m,m\in W\Rightarrow 0<m\wedge \forall m,n,(m\in W\wedge n\in W\wedge m\ne n)\Rightarrow \mathrm{Coprime}\left(m,n\right))\Rightarrow \mathrm{Surjective}\left(\mathrm{windowReading}\left(W\right)\right).$$

Proof. Machine-checked in Lean as D5/S0/Observation/FiniteWindowCRTIndistinguishability.finite_window_cannot_separate_shift (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any finite collection of positive pairwise-coprime natural moduli, the window-reading map is onto the dependent product of the corresponding residue rings. Thus one natural number realizes every prescribed residue in the window simultaneously.

The construction chooses natural representatives for the target residues, applies the finite Chinese remainder theorem, and then identifies the resulting congruences with equality in each ZMod component. The witness depends on both the finite window and the target; no single shift is asserted to realize all windows at once.

Lemma 1.2 (The four-nine-twenty-five window has an explicit certificate).

$$\mathrm{card}\left(\mathrm{ZMod}\left(4\right)\times \mathrm{ZMod}\left(9\right)\times \mathrm{ZMod}\left(25\right)\right)=900\wedge 511\equiv 3(\mathrm{mod}4)\wedge 511\equiv 7(\mathrm{mod}9)\wedge 511\equiv 11(\mathrm{mod}25).$$

Proof. Machine-checked in Lean as D5/S0/Observation/FiniteWindowCRTIndistinguishability.window_4_9_25_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

The product of the residue rings modulo four, nine, and twenty-five has exactly nine hundred elements. The natural number 511 reads as 3 modulo 4, 7 modulo 9, and 11 modulo 25.

This supplies one concrete realization in a pairwise-coprime observation window. It is an existence certificate, not a uniqueness claim and not a replacement for the general surjectivity theorem.

References

• Truth anchor: D5/S0/Observation/FiniteWindowCRTIndistinguishability.finite_window_cannot_separate_shift
• Truth anchor: D5/S0/Observation/FiniteWindowCRTIndistinguishability.window_4_9_25_certificate