periodicTranslateEncodedVertexIdxEquiv5
plain-language theorem explainer
On the canonical 5×5×5 periodic Freudenthal torus, translation of encoded vertex indices by a fixed base vertex is a bijection of the finite index set. Tensor/shear-sector proofs cite it to move gauge and normal-equation labels under longitudinal shifts. The inverse is relative translation through the vertex encoding equivalence; both compositions cancel by injectivity plus the translate/relative identities.
Claim. Let $T$ be the canonical encoded $5\times5\times5$ periodic Freudenthal torus, with vertex count $n_V$. For any base vertex $b$ on $T$, the map that sends each encoded vertex index $v\in\mathrm{Fin}(n_V)$ to the encoded index of the translate of $v$ by $b$ is a bijection $\mathrm{Fin}(n_V)\simeq\mathrm{Fin}(n_V)$.
background
Track 1.D builds the tensor/shear sector missing from the Track 1.B conformal ansatz. That ansatz assigns one scalar potential per vertex and averages endpoints to get edge-length variations; 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 canonical encoded $5\times5\times5$ periodic Freudenthal torus (PeriodicTorus5). Vertices are triples in a $5^3$ grid (PeriodicVertex5), encoded into a linear index of size $n_V$ in the numerical order used by the Track 1.D payload generators. Translation by a base vertex is the natural torus action on that grid; the encoded form is the same action written on Fin n_V.
The construction packages that encoded translation as a Lean Equiv, so downstream index bookkeeping can invert and compose shifts without ad-hoc cancellation lemmas at each use site.
proof idea
Definitional Equiv package, not a deep existence proof. Forward map is the already-defined encoded translation by the base. Inverse sends an encoded index $v$ through the vertex encoding equivalence, applies relative translation by the base on the decoded vertex, then re-encodes.
Left and right inverses each reduce by injectivity of the vertex encoding equivalence, then simp with the two cancellation identities: relative-of-translate is the identity, and translate-of-relative is the identity. No case splits on coordinates.
why it matters
Longitudinal gauge freedom on the periodic torus acts by translating vertex labels. Packaging that action as an equivalence on encoded indices is the bookkeeping primitive for moving discrete linear-algebra data (right-hand sides, normal equations) with the gauge.
The sole recorded consumer is the combined TT normal-equation index equivalence: its inverse on the vertex summand is exactly the inverse of this map. That parent object is how shear-sector residual systems stay equivariant under row-base shifts while the conformal slice is held fixed.
In the broader Recognition gravity track this is scaffolding for weak-field tensor modes beyond the scalar conformal ansatz (module Track 1.D), not a forcing-chain (T0–T8) step. It does not yet assert dynamics or a continuum TT wave equation; it only makes index translation invertible and reusable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.