periodicRelativeColumnOfRow5_endpoints
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus, endpoints of a column written in a row's relative frame equal the relative-frame images of that column's global endpoints. Tensor/shear-sector proofs cite this when moving edge data between absolute and row-centered coordinates. The argument is exhaustive case analysis on the seven nonzero cube displacements, then bit-arithmetic simplification and omega.
Claim. For edges $e,f$ on the $5\times 5\times 5$ periodic Freudenthal torus, the endpoints of the relative-frame column of $f$ with respect to $e$ equal $\bigl(\mathrm{rel}_e(v_1),\mathrm{rel}_e(v_2)\bigr)$, where $v_1,v_2$ are the global endpoints of $f$ and $\mathrm{rel}_e$ transports a vertex into the frame based at the base of $e$.
background
Track 1.D builds the tensor/shear sector missing from the Track 1.B conformal ansatz. The conformal slice assigns one scalar per vertex and averages endpoint potentials onto edges; it cannot represent pure shear, so it cannot cover transverse-traceless weak-field modes. This module separates independent edge perturbations from vertex-conformal ones and records elementary rectangle obstructions.
The ambient lattice is the encoded $5\times 5\times 5$ periodic Freudenthal torus. Edges are pairs (base vertex, nonzero cube displacement). Displacements are the seven positive bit-triples from dispBits; vertex transport uses modular addBit/addBits on each coordinate. A relative-frame column rewrites a global edge in coordinates centered at a chosen row base.
The claim equates two descriptions of that rewritten edge's endpoints: the endpoints field of the relative column, versus applying the relative-vertex map to each global endpoint of the column.
proof idea
Destructure both edges into base vertices and displacement indices, then split the bases into $(x,y,z)$ Fin-5 coordinates. Case on the column displacement (fin_cases over the seven nonzero cube directions). In each case, ext on the endpoint pair and simp unfolds the relative-column constructor, PeriodicEdge.endpoints, the relative-vertex map, modular subtraction on Fin 5, and the bit helpers addBits, dispBits, addBit, bit. Residual modular arithmetic closes by omega.
why it matters
This is a coordinate-hygiene lemma inside the tensor/shear scaffold: relative-frame edge data must have endpoints that match relative-frame vertices, or later first-variation and zero-mode arguments become ill-typed. The sole recorded consumer is periodicTranslateVertex5_relativeColumn_endpoints, whose doc-comment states that translating those relative endpoints back by the row base recovers the original global column endpoints. Together the two lemmas give a round-trip between global and row-centered edge geometry on the $5^3$ torus.
In the broader Recognition gravity track this supports independent edge (shear) perturbations beyond the conformal ansatz, the prerequisite for capturing TT gravitational-wave content that scalar vertex potentials cannot encode. It does not yet construct the TT projector or the full Regge first variation; it only locks the endpoint bookkeeping those constructions need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.