Joint Error-and-Erasure Unique Decoding

Abstract

A code of minimum distance d has a unique legal message whenever twice the unknown-error budget plus the known-erasure budget is below d.

Theorem 1.1 (The joint error-and-erasure condition gives unique decoding).

$$\begin{array}{r}\forall alpha:\mathrm{Type},[\mathrm{DecidableEq}\left(alpha\right)],\\ n,d,e,s\in \mathbb{N},\\ C:\mathrm{Set}\left(\mathrm{Fin}\left(n\right)\to alpha\right),E:\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),\\ c,r:\mathrm{Fin}\left(n\right)\to alpha,\\ \mathrm{MinDistanceAtLeast}\left(C,d\right)\wedge \mathrm{card}\left(E\right)\le s\wedge \\ 2\times e+s<d\wedge \\ c\in C\wedge \mathrm{card}\left(\{i:\mathrm{Fin}\left(n\right)\mid \neg (i\in E)\wedge r(i)\ne c(i)\}\right)\le e\Rightarrow \\ \exists x:\mathrm{Fin}\left(n\right)\to alpha,(x\in C\wedge \mathrm{card}\left(\{i:\mathrm{Fin}\left(n\right)\mid \neg (i\in E)\wedge r(i)\ne x(i)\}\right)\le e)\wedge \\ \forall y:\mathrm{Fin}\left(n\right)\to alpha,(y\in C\wedge \mathrm{card}\left(\{i:\mathrm{Fin}\left(n\right)\mid \neg (i\in E)\wedge r(i)\ne y(i)\}\right)\le e)\Rightarrow y=x.\end{array}$$

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

Source. Repository-derived.

Commentary.

Fix the known erased-coordinate finset E. A legal candidate is compatible with the received word when it disagrees on at most e coordinates outside E.

Any coordinate where two compatible candidates disagree lies either in E, in the first candidate’s unerased error set, or in the second candidate’s unerased error set. Their Hamming distance is therefore at most s + e + e. The strict bound 2e + s < d and the code’s minimum-distance condition force the candidates to coincide.

References

• Truth anchor: D5/S3/Arith/Coding/ErrorErasureUniqueDecoding.error_erasure_unique_decoding
• Dependency: D5/S3/Arith/Coding/ResidueCodeErrorDetection