periodicDispCoord5
plain-language theorem explainer
Extracts the j-th Cartesian coordinate (0 or 1) of one of the seven nonzero positive Freudenthal cube displacements on the periodic 3-torus. Gravity and Regge analysts cite it when building longitudinal gauge generators on periodic edge strains. The body is a three-way match on the coordinate index that reads the corresponding bit from dispBits.
Claim. For a displacement index $d \in \{0,\ldots,6\}$ and a coordinate index $j \in \{0,1,2\}$, return the $j$-th bit of the corresponding nonzero positive cube displacement as a real number in $\{0,1\}$.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. The conformal (vertex-scalar) ansatz cannot represent pure shear, so independent edge-length perturbations must be separated from vertex-conformal ones before transverse-traceless modes can be treated.
On the periodic Freudenthal 3-torus the seven positive edge directions are the nonzero binary vectors in ${0,1}^3$. The helper dispBits maps each index in Fin 7 to a triple of booleans encoding that direction. The present definition turns the $j$-th boolean into a real coordinate value 0 or 1, so edge strains can be dotted against coordinate axes.
This sits downstream of the PeriodicFreudenthalTorus geometry layer and feeds the concrete longitudinal gauge constructions in the same module.
proof idea
Definitional, not a proof. Unpack dispBits disp into a triple of booleans, then match on the coordinate index $j$: for $j=0,1,2$ return $1$ if the corresponding bit is true and $0$ otherwise. No lemmas are applied.
why it matters
Supplies the coordinate readout used by the finite longitudinal gauge generator on periodic edge strains: that generator takes the signed edge-direction component of a unit vector field at one vertex (positive at the head, negative at the base). The same coordinate appears in the endpoint-support identity for the longitudinal gauge map, which expands the map as a sum over the three components at base and head.
In the Recognition gravity track this is scaffolding for isolating pure shear from conformal edge perturbations, a prerequisite for covering TT gravitational-wave modes that the Track 1.B conformal ansatz cannot reach. It does not itself close the shear-sector program; it is the elementary coordinate bridge those later constructions need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.