periodicTTNormalEquationGeneratorMap5_eq_split
plain-language theorem explainer
On the encoded 5×5×5 Freudenthal torus, the combined TT normal-equation generator (coefficients on conformal vertex-deltas plus longitudinal vertex-vectors) equals the sum of the conformal generator map and the longitudinal gauge map after splitting the Sum-index coefficients. Gravity workers cite it when decomposing residuals or proving TT orthogonality. The proof unfolds the linear maps and splits the finite sum over a Sum type.
Claim. For any real coefficient assignment $c$ on the combined index set (conformal vertex indices $\oplus$ longitudinal gauge indices) and any edge $e$ of the $5\times 5\times 5$ periodic Freudenthal torus, the combined normal-equation generator at $e$ equals the conformal generator map of the conformal projection of $c$ plus the longitudinal gauge map of the gauge projection of $c$.
background
Track 1.D builds the tensor/shear sector missing from the Track 1.B conformal ansatz. That ansatz places one scalar potential per vertex and varies edge lengths by averaging endpoints; it cannot represent pure shear, so it cannot cover transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and works on the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus.
The combined normal-equation index is the disjoint union of encoded vertices (conformal delta generators) and longitudinal gauge indices (vertex-vector delta generators). Both the conformal and longitudinal maps are instances of the same finite gauge map: a coefficient vector times a family of edge perturbations, summed over the generator index. The combined generator is the same construction on the Sum-indexed family.
proof idea
Term-mode proof by unfolding. Expand the combined generator map, the conformal generator map, the longitudinal gauge map, the underlying gauge map, the two coefficient projections, and the combined generator family. After unfolding, both sides are finite linear combinations of generator values on the edge $e$. The identity Fintype.sum_sum_type rewrites the sum over Sum A B as the sum over $A$ plus the sum over $B$, which matches the conformal and longitudinal pieces exactly. No geometric lemmas are required; the equality is the Sum-decomposition of the defining sum.
why it matters
This split is the algebraic hinge for the TT normal-equation residual and for generator-space closure in the shear sector. Downstream, the residual identity writes the residual as input minus the combined generator map, so the split lets one subtract conformal and longitudinal pieces separately. The longitudinal TT subspace orthogonality theorem uses it to show a longitudinal TT perturbation is orthogonal to every combined conformal-plus-longitudinal generator. Relative TT generator closure likewise reduces translated combined generators to the fixed conformal-plus-longitudinal image via this decomposition.
In the broader Recognition gravity track, the goal is a hinge-aware Regge TT sector beyond pure conformal strain. The split keeps the already-fixed conformal and longitudinal gauges as independent summands inside the normal equations, which is the concrete bookkeeping needed before claiming a pure shear (TT) residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.