Track1DTTHessianLichnerowiczResidualRowCoeffReductionEndpoint
plain-language theorem explainer
Track 1.D residual-row coefficient endpoint: an explicit finite coefficient table for residual rows of the period-5 TT Hessian versus lattice Lichnerowicz operators is enough to obtain residual-row span, TT-kernel vanishing, kernel-row match, operator match, and the bilinear TT energy package. Track 7 handoff consumers cite this as the reduction interface for the TT shear sector. The declaration is a pure implication Prop packaging those consequences from residual-row coefficient data.
Claim. If explicit residual-row coefficient data exists for the period-5 TT Hessian and lattice Lichnerowicz kernels (a finite table assigning, to each edge-row, a conformal/longitudinal coefficient vector whose generator map recovers that residual row), then the residual rows lie in the combined generator span, the residual vanishes on longitudinal TT modes, the kernel rows match on TT, the operators match pointwise on TT modes, and the bilinear and quadratic TT energy identities follow.
background
Module setting is Gravity Track 7 fork-handoff integration: a receipt lane that records what parallel fork endpoints prove without upgrading the discovery claim. Fork A covers Track 1.B Schläfli stationarity at $N=5$; the Track 1.D material here is the TT Hessian/Lichnerowicz consequence route inside the tensor shear sector.
The comparison is between the Regge second-variation edge Hessian restricted to transverse-traceless (TT) modes and the spin-2 lattice Lichnerowicz stencil on the same period-5 edge complex. Residual-row coefficient data supplies, for each edge-row, an explicit real coefficient vector over the normal-equation index set such that the generator map of that vector equals the residual row. Residual-row span data is the weaker statement that every residual row lies in the combined conformal-plus-longitudinal generator span.
Upstream, the bilinear reduction endpoint states that once the two operators are identified pointwise on TT modes, the bilinear and quadratic TT energy matches follow for longitudinal TT edge perturbations. Kernel-row data packages the two edge-operator kernels together with the row-match identity on the TT subspace.
proof idea
Definitional packaging only: the Prop is the implication from residual-row coefficient data to the conjunction of five consequences. Nonemptiness of residual-row span data, residual-TT-zero kernel data, kernel-row data, and match data, together with the already-defined bilinear reduction endpoint. No tactics; the body is the arrow and the five-way conjunction. The companion theorem discharges the Prop by constructing each witness from coefficient data via the sector's ofRowCoeffData / ofResidualTTZeroData constructors, then invoking the bilinear endpoint.
why it matters
Closes the Track 1.D residual-row coefficient reduction interface consumed by Track 7. Downstream, the companion holds theorem asserts the Prop, and ForkHandoffIntegrationCert records the broader fork package (Tracks 1 reduction/interface, 2 many-body, 3 page capacity, 4 $w(z)$, 6 falsifier sensitivity). The cert doc stresses that Track 1 here is a reduction/interface package, not a closure of the open Schläfli displacement-class leaves.
In the gravity lane this is the sharp finite-stencil target for identifying the Regge TT Hessian with the lattice Lichnerowicz operator on period-5 TT modes, so that quadratic TT energy (shear-sector stability) inherits from the continuum Lichnerowicz form. It does not touch the forcing chain T0–T8 or the RCL directly; it sits inside the discrete gravity master-theorem handoff.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.