track1D_tt_generator_map_projector_reduction_endpoint_holds
plain-language theorem explainer
At N=5, if the periodic TT gauge map is built from finite generators, the gauge-generator, finite-generator, and projector data packages are automatically inhabited and the Freudenthal orthogonal decomposition target is available. Track 7's fork handoff certificate cites this as the Track 1.D generator-map reduction endpoint. The proof is a short term construction chaining the sector's ofGeneratorMapData / ofGaugeGeneratorData / ofFiniteGeneratorData constructors plus one orthogonal-decomposition lemma.
Claim. For every finite generator index type and every periodic transverse-traceless generator-map projector data package at $N=5$, the corresponding gauge-generator projector data, finite-generator projector data, and projector data packages are inhabited, and the Freudenthal TT orthogonal decomposition target at $N=5$ holds for that package.
background
This module is the Track 7 integration-lane receipt for parallel fork handoffs in the gravity master theorem. It records what each fork endpoint proves without upgrading the discovery claim; remaining Track 1 displacement-class leaves stay as the next dependency.
Track 1.D works in the tensor shear sector with periodic transverse-traceless (TT) data at stencil size $N=5$. The generator-map projector package packages a gauge map defined directly from finite generators. The endpoint asserts that this presentation makes the separate gauge-span proof automatic: one obtains gauge-generator projector data, then finite-generator projector data, then the ordinary projector package, plus the Freudenthal TT orthogonal decomposition target.
Upstream dimension landmarks fix spatial $D=3$ (T8/T9) and the eight-tick period $2^3$, which set the discrete recognition register against which these finite TT generator bases sit. The local claim is purely about inhabitation and reduction of projector data, not about mass ladders or coupling constants.
proof idea
Term-mode proof. Introduce the generator index type, its Fintype instance, and the generator-map projector data $D$. Promote the fintype instance, then build gauge-generator data via PeriodicTTGaugeGeneratorProjectorData5.ofGeneratorMapData D, and finite-generator data via PeriodicTTFiniteGeneratorProjectorData5.ofGaugeGeneratorData on that result. The goal is discharged by packing nonempty witnesses for those two packages, the projector package from PeriodicTTProjectorData5.ofFiniteGeneratorData, and the lemma periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_generatorMapData D. No tactic search; pure constructor chaining.
why it matters
This is the Track 1.D generator-map projector-data reduction endpoint consumed by Track 7. Downstream it is wired into forkHandoffIntegrationCert, the integration-lane certificate that aggregates fork endpoints (Schläfli reduction, disp0 base-vertex and stationary reductions, many-body amplitude-linear lift, Page-capacity, $w(z)$ band, falsifier sensitivity).
In framework terms it closes the handoff surface for the concrete vertex-vector longitudinal gauge basis: that basis is now the decomposition surface. What remains, per the sibling endpoint comment, is the coefficient projector and the reconstruction/orthogonality proof on that basis. It does not touch T5 J-uniqueness, the RCL, or the phi-ladder mass formula; it is a discrete TT shear-sector bookkeeping step needed before the master gravity theorem can treat the N=5 Freudenthal axis as fully reduced from generator maps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.