Track1DTTGramRangeCriterionReductionEndpoint
plain-language theorem explainer
Track 1.D reduction endpoint: the finite Gram range (Fredholm) criterion alone is enough to close the transverse-traceless split at N=5. Anyone citing the gravity fork handoff or the TT orthogonal decomposition will use this Prop. It packages four consequences (kernel criterion, load image, projector data, and the Freudenthal TT target) as a single implication from the range-criterion witness.
Claim. The Track 1.D Gram range-criterion reduction endpoint asserts: if the finite TT Gram operator admits range/Fredholm criterion data at $N=5$, then (i) the Gram kernel criterion is inhabited, (ii) every load lies in the Gram image, (iii) TT projector data exist for the concrete longitudinal gauge map on periodic vertex-vector indices, and (iv) the Freudenthal TT orthogonal decomposition target holds for that same gauge map (TT interpreted as finite orthogonality to conformal and gauge subspaces).
background
Module context is Gravity Track 7 fork-handoff integration: a receipt lane that records what parallel forks prove without upgrading the discovery claim. Track 1.D sits in the tensor-shear sector, where edge perturbations on the $N=5$ periodic complex are split into conformal, gauge, and transverse-traceless (TT) parts.
The honest decomposition target asks for a raw splitting such that every perturbation's three parts land in the conformal-log subspace, the gauge subspace generated by a chosen gauge map, and the TT-orthogonal complement. Here the gauge data are concrete: indices are pairs (periodic vertex, spatial component in $\mathrm{Fin},3$), and the map is the finite longitudinal generator sending coefficient vectors to edge perturbations.
Upstream, the range-criterion structure is the remaining finite-algebra input once Gram-kernel coefficient vectors are known to generate the zero edge perturbation. The kernel-criterion structure is the finite Fredholm-alternative surface: loads in the Gram image follow from annihilation of the Gram kernel plus the range criterion. Load-image data require every edge-perturbation load to lie in the image of the fixed Gram operator.
proof idea
This declaration is a pure Prop abbreviation, not a proved theorem. It wires a single implication: assume PeriodicTTGramRangeCriterionData5, conclude the conjunction of four goals. The first two are nonempty instances of kernel-criterion and load-image data; the third is nonempty TT projector data specialized to the longitudinal gauge index type and periodicLongitudinalGaugeMap5; the fourth is the Freudenthal TT orthogonal decomposition target at $N=5$ for that same gauge map. No tactics run here; the actual discharge is the sibling theorem that introduces the range witness and builds kernel, load-image, and solver data by the sector's ofRangeCriterionData / ofKernelCriterionData / ofLoadImageData constructors.
why it matters
This endpoint is the Track 1.D handoff fact consumed by Track 7. Downstream, track1D_tt_gram_range_criterion_reduction_endpoint_holds proves the Prop, and ForkHandoffIntegrationCert packages it among the fork receipts (alongside Schläfli reduction, many-body amplitude-linear lift, Page-capacity transfer, $w(z)$ band refinement, and falsifier sensitivity). The doc-comment states the mathematical point: because Gram-kernel coefficients generate zero, the finite range/Fredholm criterion alone closes the TT split.
In the broader Recognition gravity program this is interface packaging, not closure of open Schläfli or displacement-class leaves. It records that the TT projector construction and orthogonal decomposition target reduce to one finite-algebra criterion on the fixed Gram operator at $N=5$, keeping the remaining Track 1 displacement leaves as the next dependency rather than claiming a full master-theorem upgrade.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.