periodicEdgeKernelOperator5_eq_inner_row
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal edge lattice, applying a finite edge-kernel matrix to an edge perturbation at edge e equals the real inner product of that perturbation against the kernel's e-th row. Anyone comparing Regge TT Hessian stencils to lattice Lichnerowicz kernels cites this identity. The proof unfolds the three definitions and finishes by Finset sum congruence plus ring.
Claim. Let $K$ be a real matrix indexed by edges of the $5\times 5\times 5$ periodic Freudenthal torus, let $\varepsilon$ be a real-valued edge perturbation on those edges, and let $e$ be one such edge. Then the kernel-operator value $(K\varepsilon)(e)$ equals the edge inner product $\langle \varepsilon,\, K_{e,\cdot}\rangle$.
background
Track 1.D separates pure edge (tensor/shear) perturbations from the Track 1.B vertex-conformal ansatz, which cannot carry transverse-traceless gravitational-wave modes. The working geometry is the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus; edges of that torus index both perturbations and kernels.
A periodic edge operator kernel is a real matrix $K:E\times E\to\mathbb{R}$ on those edges: the concrete finite surface on which the Regge TT Hessian stencil and the lattice Lichnerowicz stencil are compared. An edge perturbation is simply a real function on the same edge set. The kernel operator at edge $e$ is the matrix-vector product row; the companion row-vector and inner-product constructions package that product as a pairing.
The module already isolates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction for the conformal ansatz. This lemma is the algebraic bridge that rewrites operator evaluation as an inner product against a fixed row.
proof idea
Term-mode proof by definitional expansion. Unfold the three abbreviations (kernel operator, edge inner product, and kernel row vector). The resulting equality is a finite sum over edges; Finset.sum_congr rfl reduces it pointwise, and each summand is an instance of commutativity/associativity of real multiplication, discharged by ring. No external lemmas are required beyond the unfolded definitions.
why it matters
Residual-kernel vanishing on TT perturbations is the compact finite target for the TT Hessian-to-Lichnerowicz comparison. The downstream structure PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5 packages a Regge Hessian kernel, a lattice Lichnerowicz kernel, and the claim that their residual annihilates the longitudinal-TT subspace; rewriting operator action as a row pairing is the natural step before residual identities are stated pointwise on edges.
In the broader Recognition gravity track this sits inside the tensor/shear sector that must eventually cover pure shear and TT modes the conformal scalar slice cannot reach. It is scaffolding algebra rather than a forcing-chain landmark (T5–T8, RCL, phi), but it is load-bearing for any certified stencil comparison on the periodic Freudenthal torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.