Full CRT Blind Count and Distance

Abstract

The full product range has maximal blind-coordinate count one below its length and exact distance one.

Theorem 1.1 (Full CRT range has no coordinate-error margin).

$$\begin{array}{c}\forall m:\mathbb{N}\to \mathbb{N},n\in \mathbb{N},\\ (0<n\wedge \\ (\forall i,j,i<j\wedge j<n\Rightarrow m\left(i\right)<m\left(j\right))\wedge \\ (\forall i,i<n\Rightarrow 2\le m\left(i\right))\wedge \\ (\forall i,j,i<n\wedge j<n\wedge i\ne j\Rightarrow \gcd (m\left(i\right),m\left(j\right))=1))\Rightarrow \\ \mathrm{maximumBlindCoordinateCount}\left(m,n,\mathrm{prefixProduct}\left(m,n\right)\right)=n-1\wedge \\ \mathrm{residueMinimumDistance}\left(m,n,\mathrm{prefixProduct}\left(m,n\right)\right)=1\wedge \\ (\forall x,y\in \mathbb{N},x<\mathrm{prefixProduct}\left(m,n\right)\wedge y<\mathrm{prefixProduct}\left(m,n\right)\wedge \mathrm{residueWord}\left(m,n,x\right)=\mathrm{residueWord}\left(m,n,y\right)\Rightarrow x=y)\wedge \\ (\exists x,y\in \mathbb{N},x<y\wedge y<\mathrm{prefixProduct}\left(m,n\right)\wedge \mathrm{hammingDist}\left(\mathrm{residueWord}\left(m,n,x\right),\mathrm{residueWord}\left(m,n,y\right)\right)=1).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Arith/Coding/FullCRTBlindCountAndDistance.full_crt_blind_count_distance_and_detection_limit (✓ std3). ∎

Source. Repository-derived.

Commentary.

The blind-coordinate count is the canonical maximum over coordinate subsets whose modulus product lies below the message range. At the full product, every prefix omitting the last coordinate is admissible, while the complete coordinate set is not.

The resulting residue words are still injective on the complete range, so encoding remains unique. The attained minimum supplies two valid words separated in exactly one coordinate, showing that a single changed coordinate can be accepted as another valid word.

References

• Truth anchor: D5/S3/Arith/Coding/FullCRTBlindCountAndDistance.full_crt_blind_count_distance_and_detection_limit
• Dependency: D5/S3/Arith/Coding/FullCRTDynamicRangeNoCorrectionMargin