periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramKernelGeneratorMapZeroData
plain-language theorem explainer
Given kernel-zero-mode data for the finite TT Gram operator on the N=5 periodic Freudenthal torus (range criterion plus every kernel coefficient vector producing the zero edge perturbation), the concrete longitudinal conformal/gauge/TT orthogonal decomposition target holds. Gravity Track 1.D and the Track 7 handoff cite this reduction. The proof is a one-line term wrapper: convert the generator-map-zero package into Gram-kernel criterion data and apply the existing criterion-to-target lemma.
Claim. Let $D$ be kernel-zero-mode data for the finite TT Gram operator on the $N=5$ periodic Freudenthal torus: the finite range (solvability) criterion for loads orthogonal to the Gram kernel, together with the assertion that every Gram-kernel coefficient vector generates the zero edge perturbation. Then the honest Track 1.D target holds for the concrete longitudinal gauge: there exists a raw edge-perturbation splitting into conformal, longitudinal-gauge, and TT parts such that every edge perturbation $\varepsilon$ has conformal part in the periodic conformal log-strain subspace, gauge part in the image of the longitudinal gauge map (indexed by vertex $\times$ spatial component in $\mathrm{Fin}\,3$), and TT part orthogonal to both the conformal and gauge subspaces.
background
Track 1.D opens the tensor/shear sector that Track 1.B's vertex-conformal ansatz cannot reach. The conformal slice assigns one scalar potential per vertex and averages endpoints onto edges; it misses pure shear and therefore cannot host transverse-traceless weak-field modes. This module separates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction for the conformal ansatz.
The decomposition target at $N=5$ asks for a raw splitting of every periodic edge perturbation into conformal, gauge, and TT pieces, with TT defined by finite orthogonality to the conformal and gauge subspaces (not continuum TT gauge fixing). The remaining load is constructing the three projectors. The concrete gauge here is longitudinal: potentials are maps from PeriodicVertex5 × Fin 3 into $\mathbb{R}$, matching spatial dimension $D=3$ forced by the forcing chain (T8).
The hypothesis package packages two facts about the finite TT Gram operator: (i) every load orthogonal to the Gram kernel lies in the Gram range, and (ii) every kernel coefficient vector maps to the zero edge perturbation. That second clause collapses residual kernel generators so the finite range criterion alone can close the target.
proof idea
One-line term proof. Convert the generator-map-zero data $D$ into Gram-kernel criterion data via PeriodicTTGramKernelCriterionData5.ofKernelGeneratorMapZeroData, then apply the already-proved lemma periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramKernelCriterionData, which states that the finite Gram range criterion is enough to close the concrete longitudinal TT decomposition target. No new projector construction occurs here; the reduction only discharges the kernel-generator side condition so the criterion lemma applies.
why it matters
This is a reduction endpoint on Track 1.D: it turns the stronger kernel-generator-map-zero package into the honest finite conformal/gauge/TT decomposition target for longitudinal gauge on the $N=5$ periodic Freudenthal torus. Downstream, track1D_tt_gram_kernel_generator_map_zero_reduction_endpoint_holds consumes it as the "explicit Gram-kernel generator-map-zero endpoint consumed by Track 7," chaining through criterion data, load-image data, and load-solver data into the master handoff.
In the Recognition gravity program this sits under the tensor/shear scaffold needed beyond the conformal ansatz, so weak-field TT content (shear, gravitational-wave-like modes on the discrete torus) can be split off gauge and conformal pieces. Spatial index type Fin 3 aligns with $D=3$ from T8. It does not yet build the three projectors from first principles; it closes the target once the Gram-kernel generator-map-zero data are supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.