periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_normalEquationData
plain-language theorem explainer
A solution of the finite normal equations on the N=5 periodic Freudenthal torus yields the orthogonal conformal/gauge/TT edge-perturbation split under the longitudinal gauge map. Track 1.D gravity and the master handoff cite this bridge. The proof is a one-line reduction through longitudinal coefficient solution data.
Claim. If $D$ is solution data for the combined finite normal equations of the $N=5$ periodic TT split (a coefficient projector whose residual is orthogonal to every normal-equation generator), then the longitudinal TT orthogonal decomposition target holds: every edge perturbation splits into conformal, longitudinal-gauge, and TT-orthogonal parts under the map sending longitudinal gauge potentials (one $\mathbb{R}^3$ component per periodic vertex) to edge perturbations.
background
Track 1.D opens the tensor/shear sector that Track 1.B's conformal ansatz cannot reach. The conformal slice assigns one scalar per vertex and averages endpoints onto edges; it misses pure shear and therefore cannot host transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction.
The decomposition target asks for a raw edge-perturbation splitting whose three summands lie in the conformal log-strain subspace, the longitudinal gauge subspace, and the TT-orthogonal complement (finite orthogonality to both conformal and gauge generators). The remaining load is construction of the three projectors.
Normal-equation solution data package that finite linear-algebra problem: a coefficient projector such that the residual of every edge perturbation is orthogonal, in the periodic edge inner product, to every normal-equation generator. Spatial dimension is the forced $D=3$ of the forcing chain (T8).
proof idea
One-line term wrapper. Convert the normal-equation solution data $D$ into longitudinal coefficient solution data via the structure map ofNormalEquationData, then apply the already-proved lemma that any such longitudinal coefficient solution closes the $N=5$ periodic Freudenthal TT orthogonal decomposition target for the longitudinal gauge map. No new algebra is performed here.
why it matters
This is the normal-equation rung of the Track 1.D projector ladder. Downstream, the Gram-system theorem reduces to it by packaging an explicit finite Gram solution as normal-equation data, and the master handoff theorem track1D_tt_normal_equation_reduction_endpoint_holds consumes it as the combined normal-equation reduction endpoint for Track 7.
In the Recognition framework it advances the weak-field metric sector beyond the conformal ansatz toward genuine TT modes on the periodic Freudenthal geometry (eight-tick / $2^3$ discrete setting with $D=3$). It does not yet exhibit the projectors by hand; it certifies that solving the finite normal system is enough to close the honest orthogonality target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.