track1D_tt_longitudinal_projector_reduction_endpoint_holds
plain-language theorem explainer
Any periodic TT longitudinal projector data at N=5 yields generator-map and coefficient projector packages plus the Freudenthal orthogonal decomposition target. Gravity Track 7 cites this as the Track 1.D handoff: the longitudinal gauge basis is the decomposition surface. The proof chains three TensorShearSector constructors and applies the longitudinal-data orthogonal-decomposition lemma.
Claim. Given periodic transverse-traceless longitudinal projector data at $N=5$, there exist a nonempty generator-map projector package on the longitudinal gauge index set, a nonempty coefficient projector package for the fixed longitudinal gauge map, and the Freudenthal TT orthogonal decomposition target at $N=5$ holds.
background
Track 7 is the fork-handoff integration lane for gravity: it records what parallel endpoints prove without upgrading the discovery claim. Track 1.D is the TT (transverse-traceless) shear-sector reduction that ends with coefficient projectors on fixed conformal and longitudinal bases.
The endpoint proposition says: from concrete longitudinal projector data on the periodic $N=5$ complex, one obtains (i) a generator-map projector package indexed by the longitudinal gauge basis, (ii) a coefficient projector package for the longitudinal gauge map, and (iii) the Freudenthal TT orthogonal decomposition target. Spatial dimension is the forced $D=3$ from the T8/T9 chain; the local geometry is the periodic Regge/TT hinge setting used throughout the shear sector.
Upstream TensorShearSector constructors turn longitudinal data into generator-map, gauge-generator, and finite-generator projector data; a companion lemma discharges the orthogonal decomposition target from the same longitudinal input.
proof idea
Term-mode proof. Introduce longitudinal projector data $D$. Build generator-map data via ofLongitudinalData, then gauge-generator data via ofGeneratorMapData, then finite-generator data via ofGaugeGeneratorData. Package the first nonempty witness as the generator-map structure; the second as the coefficient projector obtained by ofFiniteGeneratorData; the third conjunct is the lemma periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_longitudinalData applied to $D$. No further case analysis.
why it matters
Feeds forkHandoffIntegrationCert, the integration-lane certificate that assembles Track 1/2/3/4/6 handoffs. Closes the Track 1.D leaf: once the vertex-vector longitudinal gauge basis is the decomposition surface, remaining work is coefficient projectors and reconstruction/orthogonality on that basis, not a new geometric ansatz.
In the RS gravity stack this is the TT shear-sector reduction at the forced $D=3$ eight-tick geometry, aligning with the Freudenthal/Regge hinge analysis rather than continuum GR postulates. Module doc keeps displacement-class leaves as the next dependency; this theorem does not touch those leaves or the discovery claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.