periodicEdgeKernelOperator5_eq_of_kernel_eq
plain-language theorem explainer
Entrywise equality of two finite edge-operator kernels on the 5×5×5 periodic Freudenthal torus implies the induced operators agree on every edge perturbation. Anyone matching the Regge TT Hessian stencil to the lattice Lichnerowicz stencil cites this. The proof is a short reduction to the row-equality lemma, rewriting each summand by the pointwise kernel hypothesis.
Claim. Let $K$ and $L$ be real-valued kernels on pairs of edges of the $5\times 5\times 5$ periodic Freudenthal torus. If $K(e,f)=L(e,f)$ for all edges $e,f$, then for every edge perturbation $\varepsilon$ the induced operators agree: $T_K\varepsilon=T_L\varepsilon$.
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on the encoded Freudenthal triangulation. The conformal (vertex-scalar) ansatz cannot carry pure shear, so independent edge-length perturbations are needed before transverse-traceless modes can be compared to continuum spin-2 operators.
A PeriodicEdgeOperatorKernel5 is a real matrix indexed by pairs of edges of the canonical $5\times 5\times 5$ periodic torus; it is the concrete surface on which the Regge TT Hessian stencil and the lattice Lichnerowicz stencil are compared. An edge perturbation is simply a real function on those edges. The associated operator applies the kernel row-by-row as a finite sum against the perturbation.
The immediate upstream tool is the sibling row-equality lemma: if two kernels agree on every row, their operators agree. The present statement lifts that to full entrywise kernel equality.
proof idea
One short tactic proof. Apply the row-equality lemma periodicEdgeKernelOperator5_eq_of_row_eq. For each source edge, unfold the operator definition (a finite sum over target edges) and invoke Finset.sum_congr. On each summand rewrite by the pointwise hypothesis $K(e,f)=L(e,f)$. No analytic estimates or continuum limits appear.
why it matters
This is the kernel-level congruence step used when packaging Regge and Lichnerowicz data into PeriodicTTHessianLichnerowiczKernelRowData5. That structure's intended closure is to instantiate the Regge second-variation edge Hessian and the spin-2 lattice stencil, then prove the kernels match on the longitudinal-TT subspace so the operators agree on TT modes.
In the broader Recognition gravity program this sits inside Track 1.D: separating shear from the conformal ansatz so that gravitational-wave (transverse-traceless) content can be identified with a discrete Lichnerowicz operator on the Freudenthal torus. It does not itself force $D=3$ or the eight-tick octave; those enter upstream geometry. It does make the stencil comparison purely algebraic once entrywise kernel equality is known.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.