EncodedTTHessianLichnerowiczResidualEntryFormulaData5
plain-language theorem explainer
Packages the finite residual certificate for the TT sector on the canonical 5×5×5 periodic Freudenthal torus: two edge-operator kernels (Regge Hessian and lattice Lichnerowicz) plus row coefficients whose generator-map image equals their difference entrywise. Gravity workers comparing discrete Regge second variation to the continuum Lichnerowicz operator on encoded edge indices cite this surface. It is a pure data structure with an equality field, not a proved identity.
Claim. A residual-entry certificate on the encoded $N=5$ periodic Freudenthal torus consists of two real edge-operator kernels $H^{\mathrm{Regge}}, L^{\mathrm{Lich}}$ on $\mathrm{Fin}\,n_E$, together with residual row coefficients $c$ indexed by typed periodic edges and TT normal-equation generators, such that for all encoded edge indices $e,f$, $$H^{\mathrm{Regge}}_{ef}-L^{\mathrm{Lich}}_{ef}=G\bigl(c(\iota(e)),\iota(f)\bigr),$$ where $G$ is the TT normal-equation generator map and $\iota$ is the edge equivalence to typed indices.
background
Track 1.D opens the tensor/shear sector of weak-field gravity. Track 1.B's conformal ansatz puts one scalar potential per vertex and averages endpoints to get edge-length variations; that slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module isolates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction for the conformal ansatz.
The working lattice is the canonical encoded $5\times5\times5$ periodic Freudenthal torus. An encoded edge-operator kernel is simply a real matrix on $\mathrm{Fin},n_E$, the native finite edge index set of that triangulation. Typed periodic edges and the combined TT normal-equation index (conformal vertex-delta generators plus longitudinal vertex-vector generators) sit behind the encoded surface via edge and vertex equivalences.
The residual of interest is the entrywise difference between the discrete Regge Hessian kernel and the lattice Lichnerowicz kernel. The certificate asks that this residual equal the image of a coefficient row under the TT normal-equation generator map, so a finite calculation can emit an already-subtracted residual matrix and match it to a generator reconstruction.
proof idea
No proof body: this is a structure definition. It bundles four fields: the Regge Hessian kernel, the lattice Lichnerowicz kernel (both as encoded $\mathrm{Fin},n_E$ matrices), a residual row-coefficient map from typed periodic edges into the TT normal-equation dual, and a single Prop field asserting that every encoded residual entry equals the generator-map reconstruction of those coefficients after transporting indices through the torus edge equivalence. Inhabitants are built by supplying concrete kernels and coefficients and discharging the entrywise equality; the structure itself only states the certificate shape.
why it matters
In the Recognition gravity track, TT modes require a shear-capable edge sector beyond the conformal scalar slice. This certificate is the finite-index interface that lets a numerical or symbolic residual matrix be checked as exactly Regge minus Lichnerowicz and simultaneously as a linear combination of the fixed conformal and longitudinal generators. That comparison is the discrete stand-in for the continuum statement that the TT Hessian residual lies in the gauge/conformal span, which is the lattice route toward a Lichnerowicz-type identity on the Freudenthal complex.
The ambient dimension $D=3$ (forced in the RS chain) and the $N=5$ periodic torus fix the concrete index sizes. No downstream theorems yet consume the structure (used-by is empty), so it is presently a scaffold surface for forthcoming residual-kernel proofs rather than a finished link in a published forcing step. It does not itself invoke the J-cost, RCL, or phi-ladder mass formula; those enter only if later mass or coupling identifications are attached to the same torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.