periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramLoadImageData
plain-language theorem explainer
If every physical load from an edge perturbation lies in the image of the finite TT Gram operator on the N=5 periodic Freudenthal torus, the concrete longitudinal conformal/gauge/TT orthogonal decomposition target closes. Gravity-track authors cite this when reducing Track 1.D to a pure range condition. One-line term proof: lift image data to solver data and apply the solver-data closure lemma.
Claim. Given data asserting that for every edge perturbation $\varepsilon$ the associated normal-equation load lies in the image of the finite TT Gram operator on the $N=5$ periodic Freudenthal torus, the longitudinal TT orthogonal decomposition target holds: there exists a splitting of every edge perturbation into a conformal part, a longitudinal-gauge part, and a TT-orthogonal part, relative to the concrete longitudinal gauge map (vector components at periodic vertices).
background
Track 1.D opens the tensor/shear sector that Track 1.B's vertex-conformal ansatz cannot reach. The conformal slice assigns one scalar potential per vertex and averages endpoints to edge-length variations; pure shear and transverse-traceless gravitational-wave modes sit outside that slice. This module separates independent edge perturbations from vertex-conformal ones and targets a finite orthogonal decomposition on the N=5 periodic Freudenthal torus.
The decomposition target asks for a raw edge-perturbation splitting whose three summands land in the conformal log-subspace, the longitudinal gauge subspace (indexed by vertex times three spatial components, matching D=3), and the TT-orthogonal complement. The remaining load is construction of the three projectors.
Gram-load image data is the geometric range hypothesis: every load generated by an edge perturbation must lie in the image of a fixed finite TT Gram operator. It is weaker than choosing an explicit solver; it only asserts membership in the range.
proof idea
One-line term wrapper. Convert the given Gram-load image data into Gram-load solver data via the structure map ofLoadImageData, then apply the already-proved solver-data closure lemma periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramLoadSolverData. No new projector algebra is performed here; the reduction is purely data-level.
why it matters
Closes the concrete longitudinal TT decomposition target under the weakest geometric load hypothesis used on Track 1.D: pure image membership for the finite Gram operator. Downstream, the Gram-kernel criterion theorem reduces to this result by packaging kernel data as image data, and the master-theorem handoff track1D_tt_gram_load_image_reduction_endpoint_holds consumes the same image endpoint for Track 7 integration.
In the broader Recognition scaffold this is the shear-sector counterpart to the conformal ansatz: without a TT-orthogonal summand one cannot represent weak-field gravitational waves on the discrete torus. Spatial dimension D=3 (forced by T8/T9) appears in the longitudinal gauge index as the Fin-3 factor. The declaration does not invent new physics constants; it discharges a named finite-N decomposition obligation once the Gram range condition is granted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.