Track1DTTHessianLichnerowiczEncodedResidualKernelFormulaReductionEndpoint
plain-language theorem explainer
Track 1.D endpoint: an encoded residual-kernel certificate for the Regge TT Hessian versus lattice Lichnerowicz operators implies nonempty entrywise residual, row-coefficient, and match certificates, plus the bilinear TT energy reduction. Gravity auditors cite it as the residual-kernel formula handoff into Track 7. The body is a pure Prop abbreviation chaining those implications.
Claim. If an encoded residual-kernel certificate is given (Regge TT Hessian kernel, lattice Lichnerowicz kernel, residual kernel, and residual row coefficients on the $N=5$ periodic edge lattice), then there exist nonempty certificates for the encoded residual entry formula, the periodic residual entry formula, the residual-row coefficient entry equality, and the periodic TT Hessian–Lichnerowicz match, and the bilinear TT energy reduction endpoint holds.
background
Module context is Gravity Track 7 fork-handoff integration: receipts for parallel forks (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; Track 1 displacement-class leaves remain open.
The encoded residual-kernel structure packages three edge-operator kernels (Regge Hessian, lattice Lichnerowicz, residual) plus a residual row-coefficient map. Its purpose is to let a finite calculation emit the already-subtracted residual matrix, prove it equals Regge minus Lichnerowicz, and compare that residual to a generator-map reconstruction.
Upstream, the bilinear reduction endpoint states that once Regge TT Hessian and lattice Lichnerowicz agree pointwise on TT modes, bilinear and quadratic TT energies match on longitudinal TT subspace perturbations. The residual-row coefficient entry data is the scalar form: every residual kernel entry equals the corresponding generator-map reconstruction entry.
proof idea
Definitional Prop, not a proved theorem. The right-hand side is an implication: from one encoded residual-kernel data package, require nonempty witnesses for four TensorShearSector residual/match structures and conjoin the already-defined bilinear reduction endpoint. No tactics or lemmas fire here; the companion theorem later discharges the implication by constructing those witnesses via ofResidualKernelData / ofEncodedResidualKernelData converters.
why it matters
Fills the Track 1.D residual-kernel formula handoff in the fork integration lane. Downstream, the companion theorem proves this Prop holds, and ForkHandoffIntegrationCert consumes Track 1 reduction/interface packages (alongside many-body and sensitivity endpoints) without closing open Schläfli leaves. In the gravity program this is the certificate bridge from encoded residual kernels to entrywise scalar formulas and bilinear TT energy matching on the $N=5$ periodic lattice, feeding Track 7 integration rather than a master-theorem closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.