Track1DTTLongitudinalCoefficientProjectorReductionEndpoint
plain-language theorem explainer
Track 1.D endpoint: coefficient-projector data for the longitudinal TT split at N=5 already yield the longitudinal projector package, generator-map package, TT projector package on the fixed longitudinal gauge map, and the Freudenthal orthogonal decomposition target. Gravity auditors cite it when reducing remaining TT input to coefficient projectors on fixed conformal and longitudinal bases. The declaration is a Prop definition (an implication); the companion holds theorem discharges it via chained of-data constructors.
Claim. If coefficient-projector data exist for the concrete periodic longitudinal TT split at $N=5$ (conformal coefficients on vertices, gauge coefficients on longitudinal indices, and a TT projector map), then longitudinal projector data are nonempty, generator-map projector data for the longitudinal gauge index type are nonempty, full TT projector data relative to the longitudinal gauge map are nonempty, and the Freudenthal TT orthogonal decomposition target at $N=5$ holds for that gauge-potential type and map.
background
Module setting is Gravity Track 7 fork-handoff integration: a receipt lane that records what parallel forks prove without upgrading the discovery claim. Track 1.D sits in the tensor-shear sector, where TT means finite orthogonality to conformal and gauge subspaces on the periodic edge lattice at $N=5$.
Upstream, the honest decomposition target asks for a raw edge-perturbation splitting whose conformal, gauge, and TT parts land in the corresponding subspaces; the remaining load is construction of the three projectors. The longitudinal gauge index is a vertex times a spatial direction ($\mathrm{Fin},3$), and the longitudinal gauge map is the finite generator map from vertex-vector delta basis elements.
Coefficient-projector data strengthen ordinary projector data: the conformal part is generated from encoded vertex-delta coefficients rather than an arbitrary map. Generator-map projector data remove a separate gauge-span obligation by taking the gauge map itself as the span.
proof idea
Definition-only Prop: an implication whose hypothesis is the coefficient-projector structure and whose conclusion is the conjunction of three Nonempty projector packages plus the Freudenthal orthogonal decomposition target at $N=5$, all specialized to the fixed longitudinal gauge index and map. No tactics live in the body. Discharge is deferred to the companion holds theorem, which builds longitudinal data from coefficient data, then generator-map data, then gauge-generator data, and finally the target.
why it matters
Closes the Track 1.D reduction leaf that Track 7 consumes: remaining concrete TT decomposition input can be given entirely as coefficient projectors on fixed conformal and longitudinal bases. The companion holds theorem and the fork handoff integration certificate both reference this endpoint; the certificate treats Track 1 material as a reduction/interface package, not a closure of open Schläfli leaves.
In the gravity master-theorem plan this is the last packaging step before the orthogonal decomposition target is fed upward. It does not finish displacement-class stationarity or Schläfli reduction; those remain separate Track 1 leaves listed in the module doc as the next dependency. Framework-wise it is lattice gravity bookkeeping on the discrete $D=3$ side, not a constants or mass-ladder claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.