periodicEdgeKernelOperator5_residual_eq_sub
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal edge lattice, the residual kernel (Regge minus Lichnerowicz) acts as the difference of the two edge-kernel operators. Anyone comparing TT Regge Hessians to lattice Lichnerowicz stencils cites this linearity fact. The proof unfolds the finite-sum definitions and splits the sum by distributivity.
Claim. Let $K_{\mathrm{R}}, K_{\mathrm{L}}$ be real edge-to-edge kernels on the $5\times 5\times 5$ periodic Freudenthal edges, let $\varepsilon$ be a real edge perturbation, and let $e$ be a fixed edge. Writing $(K\cdot\varepsilon)(e)=\sum_f K(e,f)\,\varepsilon(f)$ and $K_{\mathrm{res}}:=K_{\mathrm{R}}-K_{\mathrm{L}}$ pointwise, one has $(K_{\mathrm{res}}\cdot\varepsilon)(e)=(K_{\mathrm{R}}\cdot\varepsilon)(e)-(K_{\mathrm{L}}\cdot\varepsilon)(e)$.
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on a periodic Freudenthal triangulation. The conformal (vertex-scalar) ansatz of Track 1.B cannot carry pure shear or transverse-traceless modes, so independent edge-length perturbations are treated as the primary variables.
Here the ambient lattice is the canonical $5\times 5\times 5$ periodic edge set. An edge perturbation is a real function on those edges. An operator kernel is a real matrix indexed by pairs of edges; the associated operator is the finite matrix-vector product $(K\cdot\varepsilon)(e)=\sum_f K(e,f),\varepsilon(f)$. The residual kernel is the pointwise difference of a Regge TT Hessian stencil and a lattice Lichnerowicz stencil, the concrete surface on which the two operators are compared.
Spatial dimension $D=3$ is the forced RS value (T8/T9), which fixes the Freudenthal cell geometry underlying the periodic torus.
proof idea
One-line conceptual content: residual operator equals difference of operators. Mechanically, unfold the operator and residual definitions to expose the finite sum $\sum_f (K_{\mathrm{R}}(e,f)-K_{\mathrm{L}}(e,f)),\varepsilon(f)$. Rewrite each summand by ring as a difference of products, then apply Finset.sum_sub_distrib to split into $\sum K_{\mathrm{R}}\varepsilon-\sum K_{\mathrm{L}}\varepsilon$. No geometric input is used.
why it matters
This is bookkeeping that unlocks the Track 1.D Hessian/Lichnerowicz match. Downstream, PeriodicTTHessianLichnerowiczKernelRowData5 packages a Regge Hessian kernel and a lattice Lichnerowicz kernel and asks that their actions agree on the longitudinal-TT subspace; the residual form of that comparison is exactly the difference identity proved here.
The module doc states the intended physical closure: on TT edge perturbations the Regge Hessian should equal the lattice Lichnerowicz operator. Showing residual action vanishes is equivalent, via this lemma, to showing the two operators coincide. In the broader RS gravity program this sits inside the weak-field tensor sector on the forced $D=3$ lattice, complementary to the conformal scalar slice of Track 1.B.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.