Reciprocity Parity Error Detection

Abstract

A valid finite sign report detects one flipped symbol but can accept two flips.

Theorem 1.1 (A parity report detects one flip but not every pair of flips).

$$\forall I:\mathrm{Type},[\mathrm{DecidableEq}\left(I\right)],S:\mathrm{Finset}\left(I\right),profile:I\to \mathrm{ZUnits},a,b:I,a\in S\wedge b\in S\wedge a\ne b\wedge \prod _{v\in S}profile(v)=1\Rightarrow (\prod _{v\in S}\mathrm{flipLocalSign}\left(profile,a,v\right)=-1\wedge \prod _{v\in S}\mathrm{flipLocalSign}\left(profile,a,v\right)=\prod _{v\in S}\mathrm{flipLocalSign}\left(profile,b,v\right)\wedge \prod _{v\in S}\mathrm{update}\left(\mathrm{flipLocalSign}\left(profile,a\right),b,-profile(b),v\right)=1).$$

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

Source. Repository-derived.

Commentary.

For a finite report of integer signs whose product is one, flipping either of two selected coordinates changes the product to minus one. The two single-error syndromes are equal, so this one check does not identify which selected coordinate was flipped.

If the two selected coordinates are distinct, flipping both restores the product to one. This supplies an explicit even-error pattern that the parity check accepts.

References

• Truth anchor: D5/S3/Arith/Coding/ReciprocityParityErrorDetection.reciprocity_parity_error_detection