Track1DTTGramRangeClosedEndpoint
plain-language theorem explainer
Packages the Track 1.D finite TT Gram-range endpoint at N=5: nonempty range, kernel, load-image, and projector data for the fixed conformal-plus-longitudinal generator family, together with the Freudenthal TT orthogonal decomposition target. Gravity Track 7 handoff and the companion holds theorem cite it. As a Prop definition it is just the conjunction of those five components; no proof lives here.
Claim. The Track 1.D closed endpoint asserts: the finite TT Gram range criterion, kernel criterion, and load-image data at $N=5$ are each inhabited; the TT projector data for the concrete longitudinal gauge map (indexed by periodic vertex $\times$ spatial component) is inhabited; and the Freudenthal TT orthogonal decomposition target holds for that same gauge potential type and map, i.e. every edge perturbation splits into conformal, gauge, and TT-orthogonal parts.
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 TT means finite orthogonality to conformal and gauge subspaces on the periodic $N=5$ edge complex.
Upstream, the decomposition target asks for a raw edge-perturbation splitting whose three parts land in the conformal log subspace, the gauge subspace of a chosen gauge map, and the TT-orthogonal complement. The concrete gauge data here are the longitudinal index type (periodic vertex $\times$ $\mathrm{Fin},3$) and the finite longitudinal gauge map generated by vertex-vector delta basis elements.
The three Gram structures are finite-algebra surfaces for one fixed TT Gram operator: range criterion (Fredholm-style: kernel-orthogonal loads lie in the image), kernel criterion (same surface phrased for the alternative), and load-image data (every load from an edge perturbation is in the Gram image). Projector data supply the concrete TT split once those criteria close.
proof idea
Definitional abbreviation only: the Prop is the five-fold conjunction of nonempty range-criterion data, nonempty kernel-criterion data, nonempty load-image data, nonempty TT projector data at the longitudinal gauge map, and the Freudenthal TT orthogonal decomposition target at that same map. No tactics or lemmas run inside the def body; discharge is deferred to the companion theorem that builds the witnesses from the proved range-criterion instance and the of-criterion constructors.
why it matters
Closes the finite Gram-range leaf of Track 1.D so the concrete TT projector split at $N=5$ can be handed to Track 7. Downstream, the holds theorem asserts this Prop, and ForkHandoffIntegrationCert consumes the Track 1 package as a reduction/interface fact among Forks A–F (not a full Schläfli closure). Module doc is explicit: remaining Track 1 displacement-class leaves stay open. In the RS gravity stack this is discrete linear-algebra infrastructure for the shear/TT sector on the eight-tick-compatible periodic complex, not a new continuum Einstein identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.