periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramSystemData
plain-language theorem explainer
A solution of the finite TT Gram system on the N=5 periodic Freudenthal torus yields the longitudinal conformal/gauge/TT orthogonal decomposition target. Gravity Track 1.D and the Track 7 handoff cite this as the Gram-system reduction endpoint. The proof is a one-line term that packages Gram data into normal-equation data and reuses the normal-equation closure.
Claim. If $D$ is explicit solution data for the finite TT Gram system on the $N=5$ periodic Freudenthal complex (a coefficient projector such that the Gram operator applied to it recovers every normal-equation load), then the concrete longitudinal TT orthogonal decomposition target holds for the longitudinal gauge potential space $\mathrm{PeriodicVertex}_5 \times \{0,1,2\} \to \mathbb{R}$ with its standard gauge map: every edge perturbation splits into conformal, longitudinal-gauge, and TT-orthogonal parts.
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on the periodic Freudenthal complex. The conformal (Track 1.B) ansatz only assigns a scalar potential per vertex and cannot represent pure shear, so it misses transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and builds a finite $N=5$ decomposition target.
The target PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5 asks for a raw edge-perturbation splitting whose three summands lie in the conformal log-strain subspace, the chosen gauge subspace, and the TT-orthogonal complement (finite orthogonality to conformal and gauge). The gauge space here is longitudinal: potentials indexed by a periodic vertex and a spatial component in $\mathrm{Fin},3$ (spatial dimension $D=3$ from T8).
PeriodicTTGramSystemSolutionData5 packages the remaining linear algebra: a coefficient projector such that the TT Gram operator applied to it equals the normal-equation load for every edge perturbation and every normal-equation index. Closing that finite Gram system is exactly what feeds the decomposition target.
proof idea
One-line term proof. Convert the Gram-system solution data $D$ into normal-equation solution data via PeriodicTTNormalEquationSolutionData5.ofGramSystemData, then apply the already-proved normal-equation closure periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_normalEquationData. No new linear algebra is done at this layer; the theorem is a packaging bridge from Gram data to the decomposition target.
why it matters
This is the Gram-system reduction endpoint for Track 1.D. Downstream, track1D_tt_gram_system_reduction_endpoint_holds in the Master Theorem handoff consumes exactly this bridge (Gram data $\to$ normal-equation data $\to$ longitudinal coefficient projectors) as the Track 7 integration point. The sibling periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramLoadSolverData further weakens the hypothesis to a load-solver interface by routing through this theorem.
In the Recognition framework the move matters because pure shear/TT modes sit outside the conformal scalar slice; without a finite orthogonal split on the Freudenthal complex, the weak-field tensor sector cannot be certified. Spatial $D=3$ (T8) enters the longitudinal gauge index as $\mathrm{Fin},3$. The remaining open work is constructing concrete Gram or load-solver data; this theorem says that once those data exist, the honest TT decomposition target is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.