periodicLongitudinalGaugeGenerator5_relativeColumn_eq_shift
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus, evaluating a longitudinal gauge generator column after a row-frame relative reindexing equals evaluating the same generator at the globally translated gauge index on the original column. Anyone building the discrete TT/shear normal equations or checking gauge covariance of edge generators will cite this. The proof is a short case-split on the (vertex, component) index followed by simp on the relative-column endpoint identities.
Claim. Let $E_5$ be the edge set of the $5\times5\times5$ periodic Freudenthal torus, and let $I_{\mathrm{lg}}=V_5\times\{0,1,2\}$ index longitudinal gauge generators (one spatial component at one vertex). For edges $r,c\in E_5$ and index $i\in I_{\mathrm{lg}}$, the longitudinal gauge generator at $i$ evaluated on the row-frame relative column of $c$ with respect to $r$ equals the generator at the base-translated index of $i$ evaluated on $c$.
background
Track 1.D opens the tensor/shear sector of the discrete weak-field metric. The older Track 1.B conformal ansatz puts one scalar at each vertex and averages endpoints to get edge-length variations; that slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module isolates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction for the conformal ansatz.
The ambient lattice is the canonical encoded $5\times5\times5$ periodic Freudenthal torus. Edges are PeriodicEdge5; longitudinal gauge indices are pairs (periodic vertex, spatial component in $\mathrm{Fin},3$). A longitudinal gauge generator is the concrete column that implements an infinitesimal longitudinal gauge move at that index. Row-frame relative columns re-express a column edge in the frame of a chosen row base; translating a gauge index by that same base is the matching global shift of the generator label.
The identity is the elementary covariance statement: relative reindexing of the column argument is interchangeable with translating the generator index.
proof idea
Destructure the longitudinal gauge index as a pair (vertex, component). The relative-column displacement equals the original column displacement by definition (rfl). Unfold the generator and the index-translation maps, then simp with the two endpoint-equality characterizations of the relative column (periodicRelativeColumnOfRow5_endpoint_fst_eq_iff and _snd_eq_iff). Those reduce both sides to the same Boolean endpoint tests against the translated vertex, so the equality is definitional after simplification.
why it matters
Longitudinal gauge columns are the pure-gauge directions that must be quotiented (or projected) when isolating physical TT/shear modes on the discrete torus. This equivariance lemma is the building block for the combined normal-equation generator identity periodicTTNormalEquationGenerator5_relativeColumn_eq_shift, whose doc-comment states the same row-frame translate equals global shift property for the full TT normal-equation basis. Without it, matrix assembly in a single row frame would not match globally shifted generator labels, breaking consistency of the discrete TT operator on the periodic lattice.
In the broader Recognition gravity track this sits under the Regge/Freudenthal discretization that supports the shear sector beyond the conformal ansatz; it is infrastructure rather than a forcing-chain landmark (T5–T8), but it is required before any claim that the discrete normal equations correctly separate gauge from TT content on the eight-tick-compatible lattice geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.