periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramLoadSolverData
plain-language theorem explainer
A finite load solver for the TT Gram operator on the N=5 periodic Freudenthal torus yields the concrete longitudinal TT orthogonal decomposition of every edge perturbation. Gravity-track authors cite it when closing Track 1.D shear coverage of weak-field TT modes. The proof is a one-line term that converts load-solver data into Gram-system solution data and reuses the existing Gram-system target theorem.
Claim. Given finite load-solver data for the TT Gram operator at $N=5$ (a map that, for every edge-perturbation load, solves the associated normal equations), the Track 1.D orthogonal decomposition target holds for the concrete longitudinal gauge: every periodic edge perturbation splits into a conformal part, a longitudinal-gauge part, and a part orthogonal to both conformal and gauge subspaces.
background
Track 1.D addresses the gap left by the Track 1.B conformal ansatz. That ansatz assigns one scalar potential per vertex and induces edge-length variations by averaging endpoints; it cannot represent pure shear and therefore cannot cover transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and builds a finite $N=5$ periodic Freudenthal setting for the tensor/shear lane.
The target proposition asserts existence of a raw edge-perturbation splitting whose three summands lie in the conformal log-subspace, the longitudinal gauge subspace (indexed by vertex times spatial direction, with spatial dimension $D=3$ from the forcing chain), and the TT-orthogonal complement relative to those two subspaces. Load-solver data packages a linear map that solves the finite TT Gram normal equations for every load arising from an edge perturbation; that is the remaining finite linear-algebra obligation once the Gram operator is fixed.
proof idea
One-line term proof. Convert the given load-solver data into Gram-system solution data via the structure map ofLoadSolverData, then apply the already-proved theorem that any Gram-system solution data closes the same longitudinal TT orthogonal decomposition target. No new linear algebra is performed here; the reduction only re-packages the hypothesis.
why it matters
This is the load-solver reduction step that lets Track 1.D hand a concrete finite endpoint to the master-theorem integration layer. Downstream, track1D_tt_gram_load_solver_reduction_endpoint_holds consumes exactly this shape of data and chains it through normal-equation and longitudinal-coefficient solution packages for Track 7. A sibling theorem also lifts the weaker load-image hypothesis to the same target by first manufacturing load-solver data, so this declaration is the common core of both closures.
In the Recognition framework it sits inside the gravity tensor/shear sector needed once the conformal scalar slice is known to be incomplete. Spatial dimension $D=3$ (T8/T9) enters the longitudinal gauge index type. The result does not invent new continuum GR; it discharges the finite $N=5$ projector-construction obligation for the honest TT-as-orthogonality reading of the decomposition target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.