periodicRelativeTTNormalEquationGeneratorMap5
plain-language theorem explainer
Defines the combined conformal-plus-longitudinal generator map rewritten in the coordinate frame of a chosen base edge on the 5×5×5 periodic Freudenthal torus. Anyone proving relative-frame TT orthogonality or generator closure cites it. The body is a one-line composition: evaluate the global generator map after translating the column edge into the row frame.
Claim. On the $5\times 5\times 5$ periodic Freudenthal torus, fix a base edge $e$ and a coefficient function $c$ on the combined index set of conformal vertex generators and longitudinal gauge generators. The relative-frame generator map sends each edge $f$ to the value of the global combined generator map at the edge obtained by expressing $f$ in the coordinate frame of $e$ (same displacement, base vertex translated relative to $e$).
background
Track 1.D isolates the tensor/shear sector of weak-field Regge gravity. 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 works with independent edge-length perturbations on the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus.
The combined normal-equation index set is the disjoint union of vertex indices (conformal generators) and longitudinal gauge indices (vertex-vector generators). The global generator map turns a coefficient vector on that index set into an edge perturbation. The relative-column map rewrites a column edge in the frame of a chosen row edge by translating the base vertex while keeping the displacement.
The present definition packages those two pieces: it is the global generator map evaluated after the column has been moved into the row frame.
proof idea
Pure definition, not a theorem. The body is the lambda
fun col => periodicTTNormalEquationGeneratorMap5 coeff (periodicRelativeColumnOfRow5 row col).
It applies the already-defined global combined generator map to the coefficient vector, but feeds it the column edge rewritten by the relative-column translation of the chosen row base. No tactics, no lemmas beyond that composition.
why it matters
Relative-frame generators are the bookkeeping device for the shifted-generator route to TT orthogonality. Downstream, PeriodicRelativeTTGeneratorOrthogonalOnTT5 asks that every longitudinal-TT edge perturbation be orthogonal (under the periodic edge inner product) to every row-frame translate of this map. PeriodicRelativeTTGeneratorClosure5 asks that every such translate split back into fixed conformal and longitudinal-gauge images.
The companion identity periodicRelativeTTNormalEquationGeneratorMap5_eq_shiftedMap rewrites the relative map as a global map with coefficients reindexed by the row-base translation equivalence, which is the algebraic bridge used in those arguments. The residual-kernel structure for the TT Hessian-to-Lichnerowicz comparison also consumes this map when stating vanishing on the TT subspace.
In the broader RS gravity track this is scaffolding for showing that the discrete Lichnerowicz operator on the Freudenthal torus has the expected TT kernel once conformal and longitudinal gauge directions are quotiented out; it does not yet touch the forcing chain (T0–T8) or continuum constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.