Track1DTTGramKernelCriterionReductionEndpoint
plain-language theorem explainer
Endpoint proposition for Track 1.D: the finite Gram-kernel criterion on the TT operator implies every physical TT load lies in the Gram image, a solver and TT projectors exist, and the Freudenthal TT orthogonal split closes at N=5. Track 7 fork-handoff certificates cite it as the packaged reduction interface. Pure Prop definition; the companion holds theorem discharges the implication chain.
Claim. If the finite TT Gram-kernel criterion data at period $N=5$ hold, then every physical TT load lies in the image of the Gram operator, a load solver exists, TT projector data exist relative to the concrete longitudinal gauge map, and the Freudenthal TT orthogonal decomposition target holds: every edge perturbation splits into conformal, gauge, and TT parts with TT finite-orthogonal to the conformal and gauge subspaces.
background
Module is the Track 7 fork-handoff integration lane: it records what parallel gravity endpoints prove without upgrading the discovery claim. Track 1.D lives in the tensor-shear sector at the fixed finite period $N=5$.
The finite TT Gram operator has a Fredholm-alternative surface: PeriodicTTGramKernelCriterionData5 says loads in the image follow once they annihilate the Gram kernel and a fixed finite-range criterion holds. Weaker geometric data (PeriodicTTGramLoadImageData5) require every load from an edge perturbation to lie in that image; solver data strengthen this to an explicit inverse. The longitudinal gauge is the concrete map from vertex-vector coefficients (PeriodicLongitudinalGaugeIdx5 → ℝ) into periodic edge perturbations.
The decomposition target interprets TT as finite orthogonality to conformal and gauge subspaces: existence of a raw splitting whose three parts land in those subspaces. Remaining mathematical load is construction of the three projectors.
proof idea
Definition-only packaging: a single implication Prop whose hypothesis is the Gram-kernel criterion structure and whose conclusion is the conjunction of nonempty load-image data, nonempty load-solver data, nonempty TT projector data for the longitudinal gauge map, and the Freudenthal TT orthogonal decomposition target at $N=5$ for that same gauge. No tactics or lemmas inside the def body; the companion theorem track1D_tt_gram_kernel_criterion_reduction_endpoint_holds walks the chain by applying the sector constructors ofKernelCriterionData, ofLoadImageData, and the Gram-system solution packaging.
why it matters
Closes the Track 1.D reduction interface that Track 7 consumes. Downstream, track1D_tt_gram_kernel_criterion_reduction_endpoint_holds proves the Prop, and ForkHandoffIntegrationCert records the handoff among Forks A–F. The cert doc is explicit: the Track 1 result is a reduction/interface package, not a closure of the open Schläfli leaves; structural master-theorem witnesses remain where the master plan requires them.
In the gravity stack this is the finite discrete stand-in for the classical TT (transverse-traceless) split of metric perturbations: once the Gram kernel is controlled, loads are solvable and the conformal/gauge/TT orthogonal decomposition exists at the eight-adjacent finite stencil $N=5$. It does not touch T5–T8 forcing, RCL, or the alpha band; it is pure gravity-track infrastructure for the master-theorem handoff.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.