Track1DTTLongitudinalCoefficientSolutionReductionEndpoint
plain-language theorem explainer
Track 1.D residual-defined coefficient-solution reduction endpoint: if a finite longitudinal coefficient solve exists whose residual is orthogonal to the conformal and longitudinal generator families, then the coefficient, longitudinal, and TT projector packages are inhabited and the Freudenthal TT orthogonal decomposition target holds at N=5 for the concrete longitudinal gauge map. Gravity auditors cite it when wiring Track 1.D into the Track 7 fork handoff. It is a pure Prop packaging of that implication, not a proved closure.
Claim. If residual-defined coefficient-solution data exist for the periodic longitudinal TT split at $N=5$ (conformal and longitudinal coefficient projectors whose residual is orthogonal to both fixed generator families), then the corresponding coefficient-projector data, longitudinal projector data, and TT projector data (for the concrete longitudinal gauge index type and gauge map) are nonempty, and the Freudenthal TT orthogonal decomposition target holds for that same gauge map.
background
Track 7 is the fork-handoff integration lane for gravity. It records what parallel endpoints prove without upgrading the discovery claim, and leaves remaining Track 1 displacement-class leaves open. Track 1.D concerns the finite TT (transverse-traceless) split of periodic edge perturbations on the $N=5$ torus.
Upstream, the honest decomposition target asks for a raw splitting into conformal, gauge, and TT parts, with TT interpreted as finite orthogonality to the conformal and gauge subspaces; the remaining load is constructing three projectors. The longitudinal gauge index type is one vector component at one periodic vertex, and the concrete longitudinal gauge map is generated by vertex-vector delta basis elements.
Coefficient-solution data state the solve with no separate TT projector: the TT part is the residual after subtracting conformal and longitudinal projections, with residual orthogonality to both generator families. Coefficient-projector data and longitudinal projector data package the corresponding maps and membership witnesses.
proof idea
Definitional Prop, not a tactic proof. The body is an implication: assume periodic TT longitudinal coefficient-solution data at $N=5$; conclude the conjunction of (i) nonempty coefficient-projector data, (ii) nonempty longitudinal projector data, (iii) nonempty TT projector data for the longitudinal gauge potential type and the concrete longitudinal gauge map, and (iv) the Freudenthal TT orthogonal decomposition target at $N=5$ for that same gauge map. The downstream holder theorem discharges it by converting solution data to coefficient data, then to longitudinal data, then to generator-map projector data, and invoking the target.
why it matters
Packages the Track 1.D residual-defined coefficient-solution reduction so Track 7 can consume it as a handoff fact. The sibling holder theorem proves the endpoint holds by the ofSolutionData / ofCoefficientData / ofLongitudinalData conversion chain. Downstream, ForkHandoffIntegrationCert integrates Forks A–F and treats the Track 1 result as a reduction/interface package, not a closure of the open Schläfli leaves. In the RS gravity program this sits under the finite shear/TT sector that supports the master structural theorem; it does not touch T5–T8 forcing, RCL, or the alpha band, but it tightens the discrete projector interface those gravity claims eventually need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.