Track1DTTLongitudinalProjectorReductionEndpoint
plain-language theorem explainer
Track 1.D handoff endpoint: given concrete longitudinal projector data on the N=5 periodic lattice, the generator-map and full TT projector packages are inhabited and the Freudenthal conformal/gauge/TT orthogonal-decomposition target holds for the vertex-vector longitudinal gauge basis. Gravity fork-integration and tensor-shear citations use this Prop. It is a pure definition packaging that implication; the companion theorem discharges it.
Claim. If concrete projector data exist for the periodic longitudinal gauge basis at $N=5$ (conformal, gauge-coefficient, and TT projectors on edge perturbations), then: (i) generator-map projector data for that finite longitudinal index type are inhabited; (ii) full TT projector data relative to the longitudinal gauge map are inhabited; and (iii) every edge perturbation admits a splitting into conformal, gauge, and TT-orthogonal parts with respect to the vertex-vector longitudinal gauge map.
background
This module is the Track 7 fork-handoff integration receipt. It records what parallel forks prove without upgrading the discovery claim; Track 1 displacement-class leaves remain open. Track 1.D lives in the tensor-shear sector on the periodic $N=5$ lattice.
The longitudinal gauge index is one vector component at one periodic vertex. The longitudinal gauge map sends coefficient functions on that finite index to edge perturbations via vertex-vector delta generators. Longitudinal projector data supply three maps: a conformal projector, a gauge-coefficient projector onto that index, and a TT projector, with membership obligations.
Upstream, the Freudenthal TT orthogonal-decomposition target at $N=5$ is the honest finite target: existence of a raw splitting whose parts lie in the conformal subspace, the gauge subspace of a chosen gauge map, and the TT-orthogonal complement. Generator-map projector data remove a separate gauge-span obligation by treating the gauge map as the span of its generators. Full TT projector data are the three projectors plus reconstruction for a general gauge operator.
proof idea
Pure Prop definition, not a proved theorem. The body is the implication from inhabited longitudinal projector data to the conjunction of three goals: nonempty generator-map projector data on the longitudinal index type; nonempty full TT projector data for the longitudinal gauge map (coefficients as the gauge potential); and the Freudenthal orthogonal-decomposition target at $N=5$ for that same gauge map. No tactics or lemmas fire here; the companion theorem track1D_tt_longitudinal_projector_reduction_endpoint_holds later builds the packages by chaining ofLongitudinalData, ofGeneratorMapData, and ofGaugeGeneratorData.
why it matters
Pins the Track 1.D reduction surface for the gravity master-theorem handoff. Downstream, the companion holds-theorem discharges this Prop, and ForkHandoffIntegrationCert consumes the Track 1 reduction/interface package alongside Track 2 many-body and Track 6 sensitivity facts. The cert doc is explicit: the Track 1 result is a reduction package, not closure of the open Schläfli leaves.
In framework terms this is lattice gravity bookkeeping on the eight-tick / discrete side: finite $N=5$ conformal/gauge/TT splitting for the longitudinal vertex-vector basis, so later stationarity and residual forks can quote a fixed decomposition surface. What remains after this endpoint is the coefficient projector and reconstruction/orthogonality proof for that basis, not a new physical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.