Track1DTTNormalEquationReductionEndpoint
plain-language theorem explainer
A single normal-equation solution on the fixed conformal-plus-longitudinal generator family closes the finite transverse-traceless decomposition at N=5. Track 7 gravity handoff cites this as the Track 1.D reduction endpoint. The definition packages the implication from normal-equation data to nonempty coefficient and projector witnesses plus the orthogonal decomposition target. Pure Prop abbreviation; the companion theorem discharges it by chaining ofNormalEquationData constructors.
Claim. If a single-system normal-equation solution exists for the concrete finite TT split on the $N=5$ periodic edge lattice, then there exist longitudinal coefficient solution data, longitudinal coefficient projector data, and TT projector data for the concrete longitudinal gauge map (vertex-vector delta generators), and the finite TT orthogonal decomposition target holds: every edge perturbation splits into conformal, gauge, and TT-orthogonal parts relative to that gauge family.
background
Module setting is Gravity Track 7 fork-handoff integration: a receipt lane that records what parallel forks prove without upgrading the discovery claim. Track 1.D is the finite TT (transverse-traceless) decomposition on the $N=5$ periodic edge lattice, with TT read as orthogonality to conformal and gauge subspaces.
Upstream, the honest decomposition target asks for a splitting of every raw edge perturbation into conformal, gauge, and TT-orthogonal parts; its remaining load is construction of the three projectors. The concrete longitudinal gauge uses index type (periodic vertex) × (Fin 3) and the generator map built from vertex-vector deltas. Normal-equation solution data is the single finite linear-algebra problem left by that track: a coefficient projector satisfying the normal equations under the periodic edge inner product.
Coefficient solution data drops a separate TT projector and takes the TT part as the residual after conformal and longitudinal projections. Coefficient projector data then packages explicit conformal and gauge coefficient maps plus a TT projector.
proof idea
Definition-only packaging: the Prop is the implication from normal-equation solution data to the conjunction of (i) nonempty longitudinal coefficient solution data, (ii) nonempty longitudinal coefficient projector data, (iii) nonempty TT projector data on the longitudinal gauge potential type and map, and (iv) the Freudenthal TT orthogonal decomposition target at N=5 for that same gauge family. No tactics; the companion theorem track1D_tt_normal_equation_reduction_endpoint_holds discharges it by intro on the normal-equation data and successive ofNormalEquationData / ofSolutionData / ofCoefficientData constructors.
why it matters
Track 1.D endpoint consumed by Track 7. It feeds track1D_tt_normal_equation_reduction_endpoint_holds and is wired into ForkHandoffIntegrationCert, the integration certificate for Forks A–F. Downstream doc states the structural master theorem still uses structural witnesses where the plan requires them, and that the Track 1 result is a reduction/interface package, not closure of the open Schläfli leaves.
In the Recognition gravity stack this records that one finite normal-equation solve on the fixed conformal-plus-longitudinal family is the remaining algebraic load for the periodic TT split at N=5. It does not touch T0–T8 forcing, RCL, or the mass ladder; it is a discrete geometric handoff inside the gravity fork tree. Open displacement-class leaves stay open; this only closes the normal-equation reduction interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.