PeriodicTTGramSystemSolutionData5
plain-language theorem explainer
Packages finite Gram-system solution data for the periodic TT split: a coefficient map from edge perturbations to normal-equation indices that solves the Gram equation for every load. Gravity Track 1.D and the MasterTheorem handoff cite it to close the TT decomposition. As a structure, it is pure data plus the universal solvability identity; no proof body.
Claim. A record consisting of a coefficient map $P$ sending each periodic edge perturbation $\varepsilon$ and each combined TT normal-equation index $i$ to a real number, together with the identity that the finite TT Gram operator applied to $P(\varepsilon)$ recovers the TT load of $\varepsilon$ at every index $i$.
background
Track 1.D opens the tensor/shear sector that Track 1.B's conformal vertex ansatz cannot reach. The conformal slice assigns one scalar per vertex and averages endpoints to edge lengths; pure shear and transverse-traceless gravitational-wave modes lie outside that slice. This module therefore treats independent edge perturbations separately from vertex-conformal ones, on the concrete periodic Freudenthal torus.
An edge perturbation is a real assignment to each typed periodic edge. The TT normal-equation index set is the disjoint sum of conformal vertex-delta generators and longitudinal vertex-vector generators. The finite Gram operator and its load functional are the discrete linear-algebra objects that encode the normal equations for the TT split on this triangulation.
The structure isolates the remaining finite linear-algebra obligation: for every load induced by an edge perturbation, exhibit coefficients that solve the Gram system.
proof idea
Definitional structure with no proof body. It declares two fields: a coefficient projector from edge perturbations and normal-equation indices into $\mathbb{R}$, and a universal equation asserting that Gram-apply of those coefficients equals the TT load at every index. Downstream constructors (e.g. ofLoadSolverData) inhabit the type by supplying an explicit solver; the structure itself only names the data contract.
why it matters
This is the Gram-system solution package that closes the finite TT split on the periodic torus. MasterTheoremHandoffIntegration consumes it in every Track 1.D reduction endpoint: load-solver, load-image, kernel-criterion, and kernel-generator-map-zero handoffs all build a PeriodicTTGramSystemSolutionData5 (via ofLoadSolverData) before producing normal-equation solutions and TT projectors.
In the Recognition gravity program, Track 1.D must cover pure shear so that weak-field TT modes are not left to the conformal ansatz alone. The structure marks the exact finite-dimensional linear-algebra cut: once every edge-perturbation load is solved against the Gram operator, the TT decomposition and projector data become available to Track 7. It sits downstream of the $D=3$ forcing (T8) only insofar as the ambient triangulation dimension is fixed; the local content is discrete Gram solvability, not a new continuum PDE theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.