Track1DTTGramKernelGeneratorMapZeroReductionEndpoint
plain-language theorem explainer
Defines the Track 1.D reduction endpoint: if every TT Gram-kernel coefficient vector maps to the zero edge perturbation, then the finite load-annihilates-kernel half of the Gram criterion, load-image data, TT projectors, and the Freudenthal TT orthogonal split at N=5 all become available. Gravity auditors cite it as the handoff Prop that Track 7 consumes. It is a pure Prop packaging, not a proved closure.
Claim. The Track 1.D endpoint asserts: if one has kernel-zero-mode data for the finite TT Gram operator (every Gram-kernel coefficient vector generates the zero edge perturbation, plus the range-of-kernel-orthogonal half), then (i) the finite TT Gram kernel-criterion data is inhabited, (ii) load-image data is inhabited, (iii) TT projector data for the concrete longitudinal gauge map on periodic $N=5$ is inhabited, and (iv) the Freudenthal TT orthogonal decomposition target holds for that same gauge potential type and longitudinal gauge map.
background
Module setting is Gravity Track 7 fork-handoff integration: receipts for parallel forks (1.B Schläfli stationarity, physical residual/Bianchi, many-body amplitude lift, Page capacity, $w(z)$ band, falsifier sensitivity). It records endpoints without upgrading the discovery claim; open Track 1 displacement-class leaves remain.
Track 1.D works in the periodic $N=5$ tensor-shear sector. TT is finite orthogonality to conformal and gauge subspaces. The honest decomposition target asks for a raw edge-perturbation splitting into conformal, gauge, and TT parts (remaining load: construct the three projectors). Gauge is the concrete longitudinal map from vertex-vector delta coefficients (index type: periodic vertex $\times$ Fin 3) to periodic edge perturbations.
The finite Fredholm surface for the TT Gram operator: loads lie in the Gram image once they annihilate the Gram kernel and a fixed finite-range criterion holds. Kernel-zero-mode data strengthens this by requiring every Gram-kernel coefficient vector to generate the zero edge perturbation, leaving only that finite range criterion.
proof idea
Definitional Prop, not a tactic proof. The body is a single implication: assume PeriodicTTGramKernelGeneratorMapZeroData5, conclude the conjunction of four facts—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 gauge map. No lemmas are applied inside the def; discharge is deferred to the companion theorem that builds criterion data from generator-map-zero data, then load-image and solver data from the criterion.
why it matters
Packages the Track 1.D Gram-kernel generator-map-zero reduction that Track 7 consumes. Downstream, track1D_tt_gram_kernel_generator_map_zero_reduction_endpoint_holds proves the Prop by constructing criterion data via ofKernelGeneratorMapZeroData, then load-image and solver data. The larger ForkHandoffIntegrationCert aggregates this class of Track 1 reduction/interface packages with Track 2 many-body and Track 6 sensitivity facts; doc-comment stresses the master theorem still uses structural witnesses and does not close open Schläfli leaves.
In the RS gravity lane this is the finite TT Gram half of the shear-sector handoff: once kernel modes map to zero edge perturbation, load annihilation becomes automatic and the orthogonal split target is on the table. It does not finish the master theorem; it narrows Track 1.D to projector construction and residual displacement-class work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.