Exact Residue-Code Minimum Distance

Abstract

The minimum Hamming distance of a bounded residue code is determined exactly by the largest product-bounded coordinate subset.

Theorem 1.1 (Exact residue-code minimum distance).

$$\begin{array}{c}\forall m:\mathbb{N}\to \mathbb{N},n,K\in \mathbb{N},\\ ((\forall i,i<n\Rightarrow 2\le m(i))\wedge \\ (\forall i,j,i<j\wedge j<n\Rightarrow m(i)<m(j))\wedge \\ (\forall i,j,i<n\wedge j<n\wedge i\ne j\Rightarrow \gcd (m(i),m(j))=1)\wedge \\ 2\le K\le \prod _{i<n}m(i))\Rightarrow \\ \mathrm{residueMinimumDistance}(m,n,K)=n-\mathrm{maximumBlindCoordinateCount}(m,n,K).\end{array}$$

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

Source. Repository-derived.

Commentary.

The minimum-distance object is the infimum of the Hamming distances between distinct messages in the bounded range. The blind-coordinate object is independently the maximum cardinality of a coordinate subset whose modulus product is below that range.

Sorting makes the first r moduli the least product among all r-coordinate subsets. The maximal blind count therefore lies between two adjacent prefix thresholds, and the frozen dynamic-range characterization turns those thresholds into the exact distance equality.

References

• Truth anchor: D5/S3/Arith/Coding/ExactResidueCodeMinimumDistance.exact_residue_code_minimum_distance
• Dependency: D5/S3/Arith/Coding/ResidueCodeDynamicRange