EncodedTTHessianLichnerowiczCoeffTranslatedFormulaData5
plain-language theorem explainer
Packages a coefficient-only certificate that the residual between the encoded Regge Hessian and discrete Lichnerowicz edge kernels on the 5×5×5 periodic Freudenthal torus equals a translated normal-equation generator map. Gravity auditors cite it as the smaller surface from which origin-column scalar formulas and TT bilinear/quadratic matches are derived. As a structure it is pure data plus one residual-entry identity, not a derived theorem.
Claim. A coefficient-only translated residual certificate on the canonical $5\times5\times5$ periodic Freudenthal torus consists of two encoded edge-operator kernels $H$ (Regge Hessian) and $L$ (lattice Lichnerowicz), together with residual generator coefficients $c:\mathrm{Fin}\,7\to I\to\mathbb{R}$ (where $I$ indexes conformal vertex-delta and longitudinal gauge generators), such that for all encoded edges $e,f$, the residual matrix entry $(H-L)_{e f}$ equals the periodic TT normal-equation generator map applied to $c(\mathrm{disp}(e))$ at the typed edge $f$.
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on a finite triangulation. The conformal (Track 1.B) ansatz assigns one scalar per vertex and cannot represent pure shear, so it misses transverse-traceless gravitational-wave modes. This module works on the canonical encoded $5\times5\times5$ periodic Freudenthal torus, with edge kernels as real matrices indexed by Fin K.nE.
An encoded edge-operator kernel is simply a map $E\times E\to\mathbb{R}$ on that finite edge set. The residual between the Regge Hessian kernel and the discrete spin-2 Lichnerowicz stencil is the object to be certified. Normal-equation indices combine conformal vertex-delta generators with fixed longitudinal vertex-vector generators; residual dispersion coefficients supply seven coefficient rows (one per edge displacement class) against those generators.
The companion origin-column certificate is a larger surface: it stores the same kernels and coefficients but also asserts origin-row scalar formulas. The present structure is strictly smaller: it only asserts the fully translated residual formula against the generator map.
proof idea
Definitional structure, not a proved theorem. Instantiation means supplying two encoded kernels, a residual coefficient table Fin 7 → PeriodicTTNormalEquationIdx5 → ℝ, and a proof of the single field encodedResidual_entry_formula: for every pair of encoded edges, the residual of the two kernels equals the periodic TT normal-equation generator map of the coefficient row for the source edge's displacement class, evaluated at the typed target edge. No algebraic reduction is performed here; downstream lemmas specialize or transport this identity.
why it matters
This is the preferred small certificate surface for the Track 1.D Hessian-to-Lichnerowicz residual. The reduction endpoint states that such data implies a nonempty origin-column coefficient certificate and the rest of the coefficient-origin route; the full-chain endpoint further exposes raw origin-column, residual origin-column/row tables, and related audit targets in one place.
In-module, match data is built from it, and the bilinear and quadratic TT energy equalities follow whenever the second (or both) edge perturbations lie in the longitudinal TT subspace. That is the concrete link from residual coefficients to operator agreement on TT modes, the sector the conformal ansatz cannot reach.
Framework-wise this sits in the gravity handoff after the forcing chain has fixed $D=3$ and the eight-tick register: it is finite-lattice operator matching on the periodic Freudenthal complex, not a continuum GR derivation. It closes a scaffold step toward certifying that the discrete Regge Hessian agrees with the lattice Lichnerowicz operator on transverse-traceless shear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.