Unique Decoding Radius

Abstract

A minimum-distance code has a unique nearby codeword below half the minimum distance, including the canonical integral correction radius.

Theorem 1.1 (Minimum distance gives the unique decoding radius).

$$\begin{gathered} \mathrm{MinDistanceAtLeast}\left(C,d\right)\Rightarrow \\ (\forall c,r,e,(c\in C\wedge \mathrm{hammingDist}\left(r,c\right)\le e\wedge 2\times e<d)\Rightarrow \exists x,x\in C\wedge \mathrm{hammingDist}\left(r,x\right)\le e\wedge \\ (\forall y,(y\in C\wedge \mathrm{hammingDist}\left(r,y\right)\le e)\Rightarrow y=x))\wedge \\ (\forall c,r,(c\in C\wedge \mathrm{hammingDist}\left(r,c\right)\le \lfloor \frac{d-1}{2}\rfloor )\Rightarrow \exists x,x\in C\wedge \mathrm{hammingDist}\left(r,x\right)\le \lfloor \frac{d-1}{2}\rfloor \wedge \\ (\forall y,(y\in C\wedge \mathrm{hammingDist}\left(r,y\right)\le \lfloor \frac{d-1}{2}\rfloor )\Rightarrow y=x)). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

If the received word and a competing codeword are each within e coordinates of the true word, the Hamming triangle inequality puts the two codewords at distance at most 2e. The strict minimum-distance bound therefore forces them to coincide.

Natural-number division makes twice floor((d - 1) / 2) strictly less than every positive d. At d = 0, radius zero still has a unique candidate because zero Hamming distance is equality.

References

• Truth anchor: D5/S3/Arith/Coding/UniqueDecodingRadius.unique_decoding_radius
• Dependency: D5/S3/Arith/Coding/ResidueCodeErrorDetection