periodicRelativeVertex5_translate_eq_self
plain-language theorem explainer
Re-basing a vertex after translating it by a fixed origin on the concrete 5×5×5 torus recovers the original relative coordinates. Anyone proving translation injectivity or building translation equivalences in the tensor/shear gravity track cites this identity. The proof destructures the product coordinates, unfolds modular add/sub, and closes with omega.
Claim. Let $b,v$ be vertices of the concrete $5\times 5\times 5$ periodic torus. Writing $b+v$ for coordinatewise translation modulo $5$ and $\mathrm{rel}_b(w)$ for the coordinates of $w$ in the frame with origin $b$, one has $\mathrm{rel}_b(b+v)=v$.
background
Track 1.D separates independent edge (shear/tensor) perturbations from the older vertex-conformal scalar ansatz, which cannot represent pure shear or TT gravitational-wave modes. The concrete working geometry is the $N=5$ periodic torus whose vertices are triples in $\mathrm{Fin},5\times\mathrm{Fin},5\times\mathrm{Fin},5$.
Coordinate addition and subtraction on each $\mathrm{Fin},5$ factor are the usual modular maps: add is $(b+v)\bmod 5$, and relative subtraction is $(v+(5-b))\bmod 5$. Translation of a vertex by a base is the product of these additions; relative re-basing is the product of the subtractions. The identity proved here is the left-inverse relation between those two maps.
proof idea
Term-mode proof. Unpack both the base and the vertex into their three $\mathrm{Fin},5$ coordinates. Apply componentwise extensionality, then simp with the definitions of translation, relative re-basing, modular add, and modular sub. Each coordinate identity reduces to an arithmetic fact on residues modulo $5$, discharged by omega.
why it matters
This is the algebraic left-inverse that makes torus translation invertible on vertices. Downstream, injectivity of translation by a fixed base is an immediate corollary: apply relative re-basing to both sides of a translation equality and rewrite with this identity. The same rewrite supplies the inverse maps in the packaged equivalences for encoded vertex-index translation and longitudinal gauge-index translation, which move discrete gauge data around the periodic cell.
In the broader Recognition gravity program this is scaffolding for the tensor/shear sector on the eight-tick / discrete-geometry side: without a clean translation action one cannot compare edge strains across cells or isolate pure shear from longitudinal gauge. It does not itself touch the conformal-rectangle obstruction or the TT zero-mode analysis, but those tracks need this torus bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.