Track1DTTFiniteGeneratorProjectorReductionEndpoint
plain-language theorem explainer
Track 1.D reduction endpoint: finite spanning-generator projector data on the N=5 periodic Freudenthal edge lattice yields full projector data and closes the conformal/gauge/TT orthogonal split. Gravity auditors and Track 7 handoff consumers cite it as the interface between finite-generator constructions and the decomposition target. The body is a pure Prop packaging of that implication; the companion theorem discharges it via ofFiniteGeneratorData.
Claim. For every gauge-potential type $G$, finite index types $C$ and $\Gamma$, and gauge map $g\colon G\to\{\text{periodic edge perturbations at }N=5\}$, if finite-generator projector data exist (three projectors built from finite spanning families of the conformal and gauge slices), then full projector data exist and the Track 1.D orthogonal decomposition target holds: every edge perturbation splits into conformal, gauge, and TT parts with the stated membership.
background
Module context is Gravity Track 7 fork-handoff integration: a receipt lane that records what parallel forks prove without upgrading the discovery claim. Fork A covers Track 1.B Schläfli stationarity at $N=5$; the present endpoint is the Track 1.D tensor-shear reduction surface feeding that integration certificate.
Edge fields live on the typed periodic Freudenthal edges at $N=5$ (PeriodicEdgePerturbation5). The honest decomposition target asks for a raw splitting into conformal, gauge, and TT parts with finite orthogonality of the TT residual to the conformal and gauge subspaces; its remaining load is constructing three projectors.
Finite-generator projector data supply those projectors from finite spanning families of the conformal and gauge slices, with TT residual orthogonal to every generator. Full projector data add membership and pointwise reconstruction obligations. The endpoint asserts that the finite-generator package is enough to obtain both nonempty full projector data and the decomposition target.
proof idea
Definitional Prop only: no proof obligations inside the declaration. It universally quantifies over gauge type, finite conformal/gauge index types, and gauge map, then packages the implication finite-generator projector data $\Rightarrow$ nonempty full projector data $\wedge$ orthogonal decomposition target.
The companion theorem track1D_tt_finite_generator_projector_reduction_endpoint_holds discharges it by introducing the data $D$ and returning the pair built from PeriodicTTProjectorData5.ofFiniteGeneratorData D together with the decomposition target proved from that construction. Treat this def as the named interface; the real work sits in the ofFiniteGeneratorData constructor and the TensorShearSector lemmas it invokes.
why it matters
Closes the Track 1.D finite-generator reduction leaf that Track 7 consumes. Downstream, track1D_tt_finite_generator_projector_reduction_endpoint_holds proves the Prop, and ForkHandoffIntegrationCert records the broader fork package (Tracks 1 reduction interfaces, Track 2 many-body, Track 6 sensitivity) without claiming Schläfli-leaf closure.
In the gravity lane this is the concrete bridge from spanning-generator constructions on the $N=5$ periodic Freudenthal stencil to the conformal/gauge/TT split used by tensor-shear analysis. It does not finish displacement-class or Schläfli stationarity leaves; the module doc keeps those as the next dependency. Framework-wise it is infrastructure for the discrete gravity master plan, not a T0–T8 forcing step or a constants claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.