encodedEdgeKernelResidual5
plain-language theorem explainer
Pointwise difference of two encoded edge-operator kernels on the finite Freudenthal triangulation: Regge minus Lichnerowicz. Anyone comparing discrete TT Hessians to continuum Lichnerowicz stencils cites this residual surface. The body is a one-line functional subtraction on Fin-indexed matrices.
Claim. Given two encoded edge-kernel matrices $K_{\mathrm{R}}, K_{\mathrm{L}} : \{0,\ldots,n_E-1\}^2 \to \mathbb{R}$ on the periodic torus triangulation, the residual kernel is the pointwise difference $(K_{\mathrm{R}}-K_{\mathrm{L}})(e,f) := K_{\mathrm{R}}(e,f) - K_{\mathrm{L}}(e,f)$.
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on a discrete triangulation. 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 separates independent edge perturbations from vertex-conformal ones and records elementary rectangle obstructions.
An encoded edge-operator kernel is a real matrix on the native finite edge index set of the encoded periodic Freudenthal triangulation (type Fin n_E → Fin n_E → ℝ). Both the discrete Regge Hessian and the lattice Lichnerowicz operator are packaged in that form so their difference is a well-typed residual kernel on the same index surface.
proof idea
Pure definition: the residual is the function sending each ordered pair of encoded edge indices to the real difference of the two input kernels at that pair. No lemmas or tactics; the companion apply lemma is rfl.
why it matters
This residual is the raw matrix surface fed into the TT Hessian/Lichnerowicz certificate structures: origin-column coefficient data, translated residual formulas, relative-frame translated formulas, and residual dispersion-row data. Those structures store the two kernels, seven residual-generator coefficient rows, and prove origin-row scalar identities and translated residual formulas against the generator map. In the gravity track, matching Regge second variation to a discrete Lichnerowicz operator on shear modes is the discrete stand-in for the continuum TT wave operator; the residual quantifies the mismatch before any claim that it vanishes or is controlled. It sits downstream of the conformal-vs-shear separation and upstream of generator-facing residual certificates, not of the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.