periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramKernelCriterionData
plain-language theorem explainer
Given finite Gram-kernel criterion data for the N=5 periodic TT Gram operator (loads annihilate the kernel and the finite Fredholm range clause holds), the concrete longitudinal conformal/gauge/TT orthogonal decomposition target is attained. Gravity Track 1.D and the Track 7 handoff cite this as the kernel-criterion entry to the Freudenthal torus splitting. The proof is a one-line term wrapper: convert kernel data to load-image data, then apply the load-image closure lemma.
Claim. If $D$ is finite Gram-kernel criterion data for the $N=5$ periodic TT Gram operator (every admissible load that annihilates the Gram kernel lies in the Gram image, and the concrete TT loads annihilate that kernel), then the longitudinal TT orthogonal decomposition target holds for the periodic longitudinal gauge map: there exists a raw edge-perturbation splitting into conformal, gauge, and TT parts, with the TT part orthogonal to the conformal and longitudinal-gauge subspaces on the $N=5$ Freudenthal torus.
background
Track 1.D opens the tensor/shear sector beyond the Track 1.B conformal ansatz. Vertex scalars induce only averaged endpoint length changes and cannot carry pure shear, so they miss transverse-traceless weak-field modes. This module separates independent edge perturbations from vertex-conformal ones and targets a finite orthogonal splitting on the periodic Freudenthal torus at $N=5$.
The decomposition target asks for a splitting of every periodic edge perturbation into conformal, gauge, and TT summands, where TT means finite orthogonality to the conformal log-strain subspace and to the image of a chosen gauge map. Here the gauge potential type is maps from longitudinal gauge indices (vertex $\times$ spatial direction in $D=3$) to $\mathbb{R}$, with the concrete periodic longitudinal gauge map.
Kernel-criterion data package the finite Fredholm alternative for the TT Gram operator: a range-from-kernel-orthogonal clause plus the statement that the physical loads annihilate the Gram kernel. Spatial dimension $D=3$ is the RS-forced value from the forcing chain (T8/T9).
proof idea
Pure term-mode one-liner. First apply the structure coercion PeriodicTTGramLoadImageData5.ofKernelCriterionData to turn kernel-criterion data into load-image data (loads lie in the Gram image). Then feed that package to the upstream closure lemma periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramLoadImageData, which already constructs the three projectors and discharges membership in the conformal, longitudinal-gauge, and TT-orthogonal subspaces. No extra tactics or case splits.
why it matters
This is the kernel-criterion gateway into the concrete $N=5$ longitudinal TT decomposition on the Freudenthal torus. Downstream, periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramKernelGeneratorMapZeroData and ..._of_gramRangeCriterionData reduce generator-map-zero and pure range criteria to this same target via the present theorem. The master handoff track1D_tt_gram_kernel_criterion_reduction_endpoint_holds consumes the kernel-criterion path explicitly for Track 7, building load-image, load-solver, and Gram-system solution data from the same package.
In the RS gravity program this advances Track 1.D past the conformal obstruction toward genuine shear/TT content needed for weak-field gravitational waves, on the $D=3$ lattice forced by the foundation chain. It does not yet finish the full projector construction in isolation; it records that the finite Gram-kernel surface is already enough to close the named decomposition target once load-image closure is available.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.