Track1DTTGaugeGeneratorProjectorReductionEndpoint
plain-language theorem explainer
Track 1.D reduction endpoint: once the conformal span is fixed by vertex generators, gauge-generator projector data on the $5\times5\times5$ periodic Freudenthal torus already yield finite-generator projector data, TT projector data, and the TT orthogonal decomposition target. Gravity Track 7 cites it in the fork-handoff certificate. The declaration is pure Prop packaging, not a proved existence theorem.
Claim. For every gauge-potential type $G$, every finite index type $I$, and every gauge map $g:G\to$ (real edge perturbations on the $N=5$ periodic Freudenthal torus), if gauge-generator projector data exist for $(G,g,I)$, then: finite-generator projector data exist (conformal indices the torus vertices), TT projector data exist, and every edge perturbation admits a splitting into conformal, gauge, and TT-orthogonal parts (the Track 1.D Freudenthal orthogonal-decomposition target).
background
Module is the Track 7 fork-handoff integration lane. It records what parallel gravity forks deliver without upgrading the discovery claim; remaining Track 1 displacement-class leaves stay open.
Track 1.D works on the canonical encoded $5\times5\times5$ periodic Freudenthal torus. Edge perturbations are real functions on the typed periodic edges. The honest decomposition target asks for a raw splitting of every edge perturbation into a conformal-log part, a gauge part (image of a gauge map), and a TT part orthogonal to both subspaces; the remaining load is constructing the three projectors.
Upstream, finite-generator projector data supply finite spanning families for the conformal and gauge slices plus projectors whose TT residual is orthogonal to every generator. Gauge-generator projector data are the thinner interface: conformal span already fixed by vertex generators, so only gauge-generator data need be supplied.
proof idea
Definitional Prop, not a tactic proof. It universally quantifies over gauge-potential type, finite gauge index type, and gauge map into $N=5$ edge perturbations, then asserts the implication: gauge-generator projector data $\Rightarrow$ nonempty finite-generator projector data (conformal index type $\mathrm{Fin}$ of the torus vertex count) $\wedge$ nonempty TT projector data $\wedge$ the Freudenthal TT orthogonal-decomposition target at $N=5$.
The companion theorem discharges the Prop by applying the structure constructor that builds finite-generator data from gauge-generator data, then packaging the three conjuncts.
why it matters
Fills the Track 1.D handoff slot in the Gravity Track 7 integration certificate. Downstream, ForkHandoffIntegrationCert consumes this endpoint among the Track 1 reduction/interface package; the companion holds-theorem is the receipt that the Prop is inhabited under the gauge-generator hypothesis.
Doc-comment states the reduction cleanly: after conformal span is fixed by vertex generators, gauge-generator projector data suffice. That matches the upstream decomposition target, whose remaining mathematical load is exactly the three projectors. It does not close open Schläfli or displacement-class leaves; the module doc keeps those as the next dependency. Framework role is gravity-side discrete TT/gauge bookkeeping on the eight-tick-compatible $N=5$ torus, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.