periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_longitudinalData
plain-language theorem explainer
Concrete longitudinal projector data on the N=5 periodic Freudenthal torus yields the finite conformal/gauge/TT orthogonal decomposition for the vertex-vector longitudinal gauge map. Gravity Track 1.D and the Track 7 handoff cite this as the longitudinal-data closure of the TT target. The proof is a one-line wrapper: convert to generator-map projector data and apply the generator-map decomposition theorem.
Claim. Given projector data for the concrete periodic longitudinal gauge basis (conformal, gauge-coefficient, and TT projectors on edge perturbations of the $N=5$ periodic torus, with the stated membership and orthogonality axioms), the finite Track 1.D TT orthogonal decomposition target holds for gauge potentials of type $\mathrm{PeriodicLongitudinalGaugeIdx}_5 \to \mathbb{R}$ under the longitudinal gauge map: every edge perturbation splits into conformal, gauge, and TT parts with the required subspace memberships.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. Track 1.B's conformal ansatz puts one scalar at each vertex and averages endpoints onto edges; that slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and records the rectangle obstruction for the conformal ansatz.
The decomposition target asserts existence of a raw edge-perturbation splitting into conformal, gauge, and TT parts, where TT means finite orthogonality (under the periodic edge inner product) to the conformal and gauge subspaces for a chosen gauge potential type and gauge map. The remaining load is constructing the three projectors.
Longitudinal projector data packages those three maps for the concrete longitudinal gauge basis, indexed by one vector component at one periodic vertex ($\mathrm{PeriodicVertex}_5 \times \mathrm{Fin},3$). Spatial dimension $D=3$ is the T8/T9 forced value used throughout the periodic geometry.
proof idea
One-line term proof. Convert the longitudinal projector data $D$ to generator-map projector data via PeriodicTTGeneratorMapProjectorData5.ofLongitudinalData, then apply periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_generatorMapData, which already closes the same decomposition target for generator-map data. No new algebraic work occurs at this layer.
why it matters
This is the longitudinal-data entry point that discharges the honest finite TT decomposition target on the N=5 periodic Freudenthal torus for the vertex-vector longitudinal gauge map. Downstream, periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_longitudinalCoefficientData reduces pure coefficient-projector data through this theorem, and track1D_tt_longitudinal_projector_reduction_endpoint_holds consumes the same longitudinal-data path as the Track 1.D reduction endpoint handed to Track 7.
In the Recognition framework this sits in the gravity tensor/shear lane needed beyond the conformal scalar slice: TT modes are the shear content that conformal vertex potentials cannot represent. The finite N=5 setting and D=3 are the discrete geometry forced by the eight-tick/T8 chain. The open mathematical load named in the target definition (constructing the three projectors) is exactly what the longitudinal projector-data structure packages and what this theorem turns into a proved Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.