periodicTranslateVertex5_relativeColumn_endpoints
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus, translating both endpoints of a column edge written in a row-edge's relative frame by that row's base recovers the original global column endpoints. Gravity/tensor-shear proofs cite it to move endpoint identities between row-relative and global coordinates. The proof rewrites the relative endpoints and cancels the translation against the relative-frame map.
Claim. Let $row$ and $col$ be edges on the $5\times 5\times 5$ periodic Freudenthal torus. Write $col$ in the coordinate frame of $row$ (same displacement, base shifted by the relative vertex of $col$ with respect to $row$). Translating both endpoints of that relative-frame edge by $row$'s base vertex yields exactly the two endpoints of the original global edge $col$.
background
Track 1.D (tensor/shear sector) separates independent edge-length perturbations from the Track 1.B vertex-conformal ansatz, which cannot represent pure shear or TT gravitational-wave modes. The concrete geometry is the encoded $5\times 5\times 5$ periodic Freudenthal torus: vertices are triples in $(\mathbb{Z}/5)^3$, and edges carry a base vertex plus a displacement.
periodicTranslateVertex5 adds two vertices componentwise mod 5. A relative-frame column periodicRelativeColumnOfRow5 row col keeps $col$'s displacement but replaces its base by the relative vertex of $col.base$ with respect to $row.base$. Upstream, periodicRelativeColumnOfRow5_endpoints states that the endpoints of this relative edge are exactly the relative-frame images of $col$'s global endpoints. Translation by the row base is the inverse of that relative map on vertices (periodicTranslateVertex5_relative_eq_self).
proof idea
Two-step tactic proof. First rewrite the relative column's endpoints via periodicRelativeColumnOfRow5_endpoints, replacing them by the pair of relative vertices of $col$'s global endpoints. Then simp with periodicTranslateVertex5_relative_eq_self cancels each translate-of-relative pair, leaving $col.endpoints$ on the nose.
why it matters
This is a small coordinate-bookkeeping lemma inside the tensor/shear scaffold: it closes the round-trip from global column endpoints to a row-relative frame and back. Downstream, periodicRelativeColumnOfRow5_endpoint_fst_eq_iff and periodicRelativeColumnOfRow5_endpoint_snd_eq_iff quote it to turn first/second endpoint equalities in the relative frame into translated global endpoint equalities (and conversely). Those iff lemmas are the natural interface when comparing shear-type edge data across neighboring rows without leaving the periodic $N=5$ torus. It does not itself encode curvature or GW polarization; it only keeps endpoint identities coherent so later shear-versus-conformal comparisons stay well-typed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.