Arbitrary Error Correction Capacity

Abstract

Disjoint radius-e Hamming balls force distance 2e+1 and the corresponding mixed-modulus capacity bound.

Theorem 1.1 (Arbitrary error correction forces the capacity bound).

$$\begin{gathered} \forall m:\mathbb{N}\to \mathbb{N},\forall n,K,e\in \mathbb{N}, \\ (\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)\wedge 2\le K\wedge \\ (\forall x,y,r,(x<K\wedge y<K\wedge \mathrm{hammingDist}\left(r,\mathrm{residueWord}\left(m,n,x\right)\right)\le e\wedge \mathrm{hammingDist}\left(r,\mathrm{residueWord}\left(m,n,y\right)\right)\le e)\Rightarrow x=y) \\ \Rightarrow \mathrm{MinDistanceAtLeast}\left(m,n,K,2\times e+1\right)\wedge \\ K\le \mathrm{prefixProduct}\left(m,n-2\times e\right). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The correction premise is operational: any received word within e coordinates of two residue codewords forces their messages to coincide. Splitting the disagreement coordinates between two candidate words shows that their distance cannot be at most 2e.

The existing exact dynamic-range theorem then converts minimum distance 2e+1 into the product of the first n-2e moduli. The result does not need the ambient upper bound K at most the full modulus product.

References

• Truth anchor: D5/S3/Arith/Coding/ArbitraryErrorCorrectionCapacity.arbitrary_error_correction_capacity_bound
• Dependency: D5/S3/Arith/Coding/ResidueCodeDynamicRange