Two-Four-Gap Modulo-Three Curvature

Abstract

Two-four-gap constellations omit a residue modulo three exactly when every adjacent curvature is nonzero.

Theorem 1.1 (Modulo-three admissibility is equivalent to nonzero gap curvature).

$$\begin{array}{c}\forall H\in \mathrm{List}(\mathbb{Z}),\\ (\forall i\in \mathbb{N},i+1<\mathrm{length}(H)\Rightarrow (H_{i+1}-H_i=2\vee H_{i+1}-H_i=4))\Rightarrow \\ (((\exists r\in \mathrm{ZMod}(3),\forall i\in \mathbb{N},i<\mathrm{length}(H)\Rightarrow \mathrm{residue}(3,H_i)\ne r)\iff \forall i\in \mathbb{N},i+2<\mathrm{length}(H)\Rightarrow (\frac{H_{i+1+1}-H_{i+1}}{2}-1)-(\frac{H_{i+1}-H_i}{2}-1)\ne 0)\wedge \\ \forall i\in \mathbb{N},i+2<\mathrm{length}(H)\Rightarrow \\ (((\frac{H_{i+1+1}-H_{i+1}}{2}-1)-(\frac{H_{i+1}-H_i}{2}-1)=0\iff (H_{i+1}-H_i=H_{i+1+1}-H_{i+1}\wedge \forall r\in \mathrm{ZMod}(3),\mathrm{residue}(3,H_i)=r\vee \mathrm{residue}(3,H_{i+1})=r\vee \mathrm{residue}(3,H_{i+2})=r))\wedge \\ ((\frac{H_{i+1+1}-H_{i+1}}{2}-1)-(\frac{H_{i+1}-H_i}{2}-1)=1\iff (H_{i+1}-H_i=2\wedge H_{i+1+1}-H_{i+1}=4\wedge \exists r\in \mathrm{ZMod}(3),\mathrm{residue}(3,H_i)\ne r\wedge \mathrm{residue}(3,H_{i+1})\ne r\wedge \mathrm{residue}(3,H_{i+2})\ne r))\wedge \\ ((\frac{H_{i+1+1}-H_{i+1}}{2}-1)-(\frac{H_{i+1}-H_i}{2}-1)=-1\iff (H_{i+1}-H_i=4\wedge H_{i+1+1}-H_{i+1}=2\wedge \exists r\in \mathrm{ZMod}(3),\mathrm{residue}(3,H_i)\ne r\wedge \mathrm{residue}(3,H_{i+1})\ne r\wedge \mathrm{residue}(3,H_{i+2})\ne r)))).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let H be a finite integer constellation whose consecutive gaps are all two or four. Its normalized curvature at a triple is the second gap bit minus the first gap bit.

The constellation omits a residue modulo three exactly when every adjacent curvature is nonzero. Equal gaps have zero curvature and their three points cover all residues.

A two-then-four turn has curvature one, while a four-then-two turn has curvature minus one. Each unequal turn visits only two residues and therefore has an explicitly omitted residue.

Repository and pinned-library searches found no exact theorem. The proof constructs the residue trajectory from the integer gaps, proves its two-step repetition, and classifies all four local gap pairs.

References

• Truth anchor: D5/S3/Arith/Congruence/TwoFourGapModThreeCurvature.two_four_gap_mod_three_admissible_iff