periodicTranslateVertex5_injective
plain-language theorem explainer
On the concrete 5×5×5 periodic torus, translation by any fixed base vertex is an injective map of vertices. Anyone working the tensor/shear sector or periodic edge frames will cite this when moving endpoint equalities between global and row-relative coordinates. The proof is a short term argument: apply the relative-coordinate map and cancel translation via the re-basing identity.
Claim. Fix a base vertex $b$ on the periodic $5\times 5\times 5$ torus. The translation map $v \mapsto b+v$ (componentwise modular arithmetic on each $\mathrm{Fin}\,5$ coordinate) is injective: if $b+v=b+w$, then $v=w$.
background
Track 1.D builds the tensor/shear sector beyond the Track 1.B conformal ansatz. The conformal slice assigns one scalar potential per vertex and cannot represent pure shear, so it misses transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and records elementary rectangle obstructions.
PeriodicVertex5 is the type of vertices of the discrete $5\times 5\times 5$ torus (Vertex 5 5 5). Translation by a fixed base and the relative-coordinate map (coordinates of $v$ in the frame with origin at the base) are the elementary group actions on that torus. The upstream identity states that re-basing a translated vertex at the same origin recovers the original relative vertex: relative coordinates undo translation.
proof idea
Term-mode injectivity proof. Assume periodicTranslateVertex5 base v = periodicTranslateVertex5 base w. Apply congrArg of periodicRelativeVertex5 base to both sides. The lemma periodicRelativeVertex5_translate_eq_self rewrites each side to $v$ and $w$ respectively, so simpa finishes $v=w$. No case splits on coordinates are needed at this layer.
why it matters
Injectivity of base translation is the algebraic hinge that lets endpoint comparisons move cleanly between global and row-relative frames. Downstream, the two endpoint-equality equivalences for periodicRelativeColumnOfRow5 quote it: first (resp. second) endpoint equality in a row-relative frame is equivalent to translated global endpoint equality. Those lemmas sit in the shear-sector scaffolding that isolates non-conformal edge strains on the periodic torus, the discrete setting needed before TT-mode bookkeeping can be stated. Within RS gravity this is infrastructure for Track 1.D, not a forcing-chain landmark (T5–T8), but it is required before shear can be separated from the conformal ansatz on the concrete lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.