Even Dense Constellation Mirror Code

Abstract

An even two-four-gap constellation that omits a residue modulo three has a reversal-fixed gap code.

Theorem 1.1 (The gap code of an even admissible dense constellation is self-reversing).

$$\begin{array}{c}\forall H\in \mathrm{List}\left(\mathbb{Z}\right),\\ ((\forall i\in \mathbb{N},i+1<\mathrm{length}\left(H\right)\Rightarrow (H_{i+1}-H_i=2\vee H_{i+1}-H_i=4))\wedge \\ (\exists r\in \mathrm{ZMod}\left(3\right),\forall i\in \mathbb{N},i<\mathrm{length}\left(H\right)\Rightarrow \mathrm{residue}\left(3,H_i\right)\ne r)\wedge \\ \mathrm{Even}\left(\mathrm{length}\left(H\right)\right))\Rightarrow \\ \mathrm{reverse}\left(\mathrm{zipWith}\left((u,v\mapsto \mathrm{decide}\left(v-u=4\right)),H,\mathrm{tail}\left(H\right)\right)\right)=\mathrm{zipWith}\left((u,v\mapsto \mathrm{decide}\left(v-u=4\right)),H,\mathrm{tail}\left(H\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Arith/Congruence/EvenDenseConstellationMirrorCode.even_dense_constellation_gap_code_self (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let points be an integer constellation whose consecutive gaps are all two or four. If one residue modulo three is omitted, two consecutive gaps cannot agree: three points separated by equal gaps would visit every residue.

The constructed Boolean gap code therefore alternates. An even number of points gives the code odd length, so reversing it preserves every symbol.

References

• Truth anchor: D5/S3/Arith/Congruence/EvenDenseConstellationMirrorCode.even_dense_constellation_gap_code_self