Track1DTTHessianLichnerowiczResidualTTZeroReductionEndpoint
plain-language theorem explainer
Track 1.D residual-kernel zero reduction: if the residual edge kernel ReggeTT minus LichnerowiczTT annihilates every transverse-traceless perturbation, then the TT Hessian–Lichnerowicz kernel-row and match data exist and the bilinear TT-energy match endpoint follows. Gravity auditors cite it as the residual-zero leaf of the Track 1.D handoff into Track 7. It is a pure Prop abbreviation chaining residual-zero data into the bilinear endpoint.
Claim. If the residual edge kernel $\mathrm{Regge}_{TT}-\mathrm{Lichnerowicz}_{TT}$ annihilates every transverse-traceless (TT) edge perturbation on the $N=5$ periodic lattice, then there exist nonempty kernel-row data and match data identifying the Regge TT Hessian with the lattice Lichnerowicz operator on TT modes, and the bilinear/quadratic TT-energy match endpoint holds.
background
This module is the Track 7 fork-handoff integration lane. It records what parallel gravity forks prove without upgrading the discovery claim, and keeps remaining Track 1 displacement-class leaves open.
Track 1.D concerns matching the Regge second-variation TT Hessian to the spin-2 lattice Lichnerowicz operator on periodic $N=5$ edge perturbations. Upstream, the bilinear reduction endpoint states that once those operators are identified pointwise on TT modes, the bilinear and quadratic TT energy matches follow. Kernel-row data package a Regge Hessian kernel and a lattice Lichnerowicz kernel together with a row-match hypothesis on the longitudinal TT subspace.
The residual-zero hypothesis is the stronger leaf: the difference kernel itself annihilates every TT mode. That is the intended physical closure path for proving the operator match without a full stencil-by-stencil expansion of both sides.
proof idea
Definitional Prop, not a proved theorem. The body is an implication: residual TT-zero data implies the conjunction of nonempty kernel-row data, nonempty match data, and the bilinear reduction endpoint. No tactics; the companion theorem track1D_..._holds later discharges it by building row data from residual-zero data via ofResidualTTZeroData and packaging the resulting witnesses.
why it matters
This is the residual-kernel zero endpoint consumed by Track 7. Downstream, the companion holds-theorem asserts the Prop, and ForkHandoffIntegrationCert packages Track 1 reduction/interface facts alongside Track 2 many-body and Track 6 sensitivity handoffs. The cert doc is explicit: Track 1 here is a reduction package, not closure of the open Schläfli leaves.
In the gravity program this isolates the cleanest TT-sector leaf of the Regge-to-continuum match: residual annihilation on TT modes, rather than full operator equality off the TT subspace. It does not touch the forcing chain (T0–T8), RCL, or the alpha band; it is a discrete-gravity handoff inside the master-theorem integration lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.