Dense Gap Mirror Parity

Abstract

Dense admissible integer configurations have parity-controlled reflection.

Theorem 1.1 (Point-count parity determines the reflected gap code).

$$\forall gapCount\in \mathbb{N},offset\in \mathrm{Fin}\left(gapCount+1\right)\to \mathbb{Z},\left(\left(\forall i\in \mathrm{Fin}\left(gapCount\right),offset\left(\mathrm{succ}\left(i\right)\right)-offset\left(\mathrm{castSucc}\left(i\right)\right)=2\vee offset\left(\mathrm{succ}\left(i\right)\right)-offset\left(\mathrm{castSucc}\left(i\right)\right)=4\right)\wedge \left(\neg \mathrm{Surjective}\left((i:\mathrm{Fin}\left(gapCount+1\right)\mapsto \mathrm{cast}\left(offset\left(i\right),\mathrm{ZMod}\left(3\right)\right))\right)\right)\right)\Rightarrow \mathrm{let}gapCode:\mathrm{List}\left(\mathrm{Bool}\left(\right)\right):=\mathrm{ofFn}\left((i:\mathrm{Fin}\left(gapCount\right)\mapsto \mathrm{decide}\left(offset\left(\mathrm{succ}\left(i\right)\right)-offset\left(\mathrm{castSucc}\left(i\right)\right)=4\right))\right),\left(\mathrm{Even}\left(gapCount+1\right)\Rightarrow \mathrm{reverse}\left(gapCode\right)=gapCode\right)\wedge \left(\mathrm{Odd}\left(gapCount+1\right)\Rightarrow \mathrm{reverse}\left(gapCode\right)=\mathrm{map}\left(not,gapCode\right)\right)$$

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

Source. Repository-derived.

Commentary.

The configuration has gapCount plus one ordered integer offsets. Every adjacent gap is two or four, and the offsets do not cover every residue modulo three.

The Boolean gap code is constructed by recording four-gaps as true. Mod-three admissibility forces alternation; reflection fixes the code at even point count and complements it at odd count.

References

• Truth anchor: D5/S3/Arith/Congruence/DenseGapMirrorParity.dense_gap_mirror_parity
• Dependency: D5/S3/Arith/Congruence/EvenDenseConstellationMirrorCode