encodedEdgeKernelResidual5_apply
plain-language theorem explainer
On the encoded 5×5×5 periodic Freudenthal edge index set, the residual kernel between a Regge Hessian and a lattice Lichnerowicz operator is pointwise their difference. Anyone comparing discrete TT Hessians to continuum Lichnerowicz kernels on this triangulation cites it. The proof is pure definitional equality (rfl).
Claim. For any two encoded edge-operator kernels $R,L$ on the $5\times 5\times 5$ periodic Freudenthal torus (maps $\mathrm{Fin}\,n_E\times\mathrm{Fin}\,n_E\to\mathbb{R}$) and any edge indices $e,f$, the residual kernel satisfies $(R-L)(e,f)=R(e,f)-L(e,f)$.
background
Track 1.D opens the tensor/shear sector of the weak-field gravity program. Track 1.B's conformal ansatz puts one scalar at each vertex and averages endpoints to get edge strains; that slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module isolates independent edge perturbations and records elementary rectangle obstructions to vertex-conformality.
The working geometry is the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus. An encoded edge-operator kernel is simply a real matrix indexed by the finite edge set $\mathrm{Fin},n_E$ of that triangulation. The residual kernel is defined by pointwise subtraction of a Regge-side kernel from a lattice Lichnerowicz kernel on that same index surface, giving a native finite-index certificate object for TT residual formulas.
proof idea
One-line definitional proof. The residual is defined as fun e f => reggeKernel e f - lichnerowiczKernel e f, so evaluating it at any pair of encoded edge indices is definitionally the corresponding difference; rfl closes the goal.
why it matters
Feeds the structure EncodedTTHessianLichnerowiczResidualEntryFormulaData5, the certificate surface for raw scalar TT residual formulas on the encoded $N=5$ edge indexing. That structure packages Regge Hessian and lattice Lichnerowicz kernels together with an entry-wise residual formula; this lemma is the trivial but necessary unfolding step that lets residual entries be rewritten as kernel differences without extra hypotheses.
In the broader Recognition gravity track it sits under the tensor/shear scaffold that must eventually cover TT modes the conformal ansatz cannot reach. It does not itself force $D=3$ or the eight-tick octave; it is local discrete-operator bookkeeping on the fixed $5^3$ torus used for numerical and formal residual checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.