periodicRelativeTTNormalEquationGeneratorMap5_eq_shiftedMap
plain-language theorem explainer
Relative-frame TT normal-equation generator maps equal ordinary generator maps after reindexing coefficients by the row-base translation. Anyone proving generator-space closure in the relative frame on the 5³ Freudenthal torus cites this identity. The proof unfolds both maps and reindexes the finite sum via the translation equivalence plus a relative-column shift lemma.
Claim. For every edge $row$ and column $col$ on the $5\times 5\times 5$ periodic Freudenthal torus and every coefficient vector $c$ on the combined conformal-plus-longitudinal generator index set, the relative-frame generator map at $row$ equals the ordinary generator map on the coefficient vector pulled back by the inverse of the row-base translation equivalence: $G^{\mathrm{rel}}_{row}(c,col)=G(c\circ\sigma_{row}^{-1},col)$.
background
Track 1.D opens the tensor/shear sector of weak-field gravity on the periodic Freudenthal torus. The conformal ansatz of Track 1.B assigns one scalar 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.
The ambient lattice is the encoded $5\times 5\times 5$ periodic edge set. Combined normal-equation indices are the disjoint union of fixed conformal vertex-delta generators and fixed longitudinal vertex-vector generators. Translation of a combined index by a typed row base moves conformal indices by the encoded vertex equivalence and translates the vertex of a gauge index while preserving its vector component.
Relative-frame maps evaluate generators on a column expressed in the frame of a chosen row edge. The ordinary map uses a fixed global frame. The claim equates the two after coefficient reindexing.
proof idea
Classical mode. Let $\sigma$ be the row-base translation equivalence on combined indices. Unfold the relative map, the ordinary map, and the underlying gauge generator map. The first calc step rewrites the summand by the relative-column shift identity: the generator at a relative column equals the generator at the translated absolute index, then uses Finset.sum_congr. The second step applies Fintype.sum_equiv along $\sigma$, moving $\sigma$ from the generator index onto the coefficient via $\sigma^{-1}$. The pointwise witness is a one-line simp on $\sigma$.
why it matters
This is the missing shifted-generator lemma for the relative-frame route: every TT perturbation must be shown orthogonal to every row-frame translate of the combined conformal/longitudinal generator map. Downstream, periodicRelativeTTGeneratorClosure5_holds builds the shifted coefficient $c\circ\sigma^{-1}$ and invokes this equality to prove that the row-frame translated combined generator space is exactly closed inside the fixed conformal-plus-longitudinal image.
In the broader Recognition gravity program this is scaffolding for the tensor/shear sector that must eventually carry TT modes beyond the conformal slice. It does not yet touch the forcing chain (T5–T8) or the mass ladder; it is local linear-algebra bookkeeping on the discrete torus needed before a discrete Lichnerowicz or Regge TT analysis can close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.