periodicTranslateEncodedVertexIdx5
plain-language theorem explainer
On the canonical 5×5×5 periodic Freudenthal torus, this maps an encoded vertex index to the encoded index of its translate by a typed base vertex. Anyone relating row-relative edge frames to the global lattice (conformal generators, endpoint identities, TT normal-equation indices) cites it. The body is pure transport: decode, apply typed translation, re-encode.
Claim. Let $T$ be the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus, with vertex set identified with $\mathrm{Fin}\, n_V$ via a fixed equivalence $\Phi$. For a typed base vertex $b$ and an encoded index $v\in\mathrm{Fin}\, n_V$, the translated encoded index is $\Phi^{-1}\bigl(\tau_b(\Phi(v))\bigr)$, where $\tau_b$ is lattice translation by $b$ on the typed vertex set.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. Track 1.B's conformal ansatz puts one scalar at each vertex and averages endpoints to get edge strains; that slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction.
The working lattice is the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus. Typed vertices are Vertex 5 5 5; encoded indices live in Fin n_V with the external order $((x\cdot 5+y)\cdot 5+z)$. A fixed equivalence $\Phi$ converts between the two presentations. Translation by a typed base is already defined on typed vertices; the present map is the same operation written entirely in encoded indices.
proof idea
One-line definition by transport. Decode the input index with the canonical vertex equivalence, apply the existing typed periodic translation by the base vertex, then re-encode with the inverse equivalence. No further lemmas are invoked in the body.
why it matters
Encoded translation is the bookkeeping primitive that lets row-relative frames talk to the global lattice without leaving Fin n_V. Downstream it appears in: the identity that a row-frame translate of a conformal generator column equals the globally shifted column; the two iff-statements equating encoded endpoint membership in a relative frame with shifted endpoints in the global frame; the packaging of this map as a lattice equivalence; and the translation of combined TT normal-equation generator indices (conformal summands shift by this map; gauge summands shift the vertex and keep the vector component).
In the Recognition gravity track this is scaffolding for the shear/TT sector beyond the conformal ansatz, not a forcing-chain step (T5–T8). It does not itself produce wave modes; it only makes index arithmetic coherent for later generator and kernel arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.