Track1DTTGramSystemReductionEndpoint
plain-language theorem explainer
Solving the explicit finite Gram system for the periodic TT split at N=5 yields normal-equation data, longitudinal coefficients, TT projectors, and closes the finite orthogonal decomposition. Track 7 gravity handoff cites this as the Track 1.D reduction endpoint. The declaration is a Prop packaging that implication from Gram-system solution data to the four downstream witnesses.
Claim. If the explicit finite Gram system for the periodic transverse-traceless split at $N=5$ admits a solution, then the combined normal equations are solvable, the longitudinal gauge coefficients exist, the TT projectors exist for the concrete longitudinal gauge map, and the finite Freudenthal TT orthogonal decomposition target (TT as orthogonality to conformal and gauge subspaces) holds.
background
Track 7 is the integration-lane receipt for parallel fork handoffs in the gravity master theorem. It records what each fork endpoint proves without upgrading the discovery claim. Track 1.D sits in the tensor-shear sector: finite edge perturbations on the periodic $N=5$ complex, split into conformal, gauge, and transverse-traceless (TT) parts.
The honest decomposition target interprets TT as finite orthogonality to the conformal-log and gauge subspaces; the remaining load is constructing three projectors. The concrete longitudinal gauge is indexed by vertex-vector pairs and generated by delta basis elements on edges. Gram-system solution data supply a coefficient projector satisfying the explicit finite Gram identities for that split.
Upstream, normal-equation data package the single finite linear-algebra problem left by the decomposition track. Longitudinal coefficient data state the same solve with TT recovered as the residual after conformal and longitudinal projections.
proof idea
Pure definition: the body is the implication Prop itself, not a proved theorem. Antecedent is existence of explicit Gram-system solution data at $N=5$. Consequent is the conjunction of four facts: nonempty normal-equation solution data, nonempty longitudinal-coefficient solution data, nonempty TT projector data for the concrete longitudinal gauge index type and map, and the Freudenthal TT orthogonal decomposition target at $N=5$ for that same gauge map. No tactics or lemmas are applied here; discharge lives in the companion theorem that builds the four witnesses from Gram data via the ofGramSystemData / ofNormalEquationData / ofSolutionData constructors.
why it matters
This is the Track 1.D handoff leaf consumed by Track 7. The companion theorem track1D_tt_gram_system_reduction_endpoint_holds proves the Prop, and ForkHandoffIntegrationCert records it among the fork endpoints (alongside Schläfli reduction, many-body amplitude-linear lift, Page-capacity transfer, $w(z)$ falsifier band, and Track 6 sensitivity).
In the Recognition gravity program the finite TT split is the discrete stand-in for the continuum transverse-traceless gauge used in linearized GR and gravitational-wave extraction. Closing the Gram-system reduction means the finite linear algebra of the shear sector is reduced to an explicit, checkable system rather than an abstract existence claim.
It does not finish Track 1: the module doc keeps the remaining displacement-class and Schläfli leaves as open dependencies. The structural master theorem still uses structural witnesses where the plan requires them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.