periodicEdgeKernelOperator5_eq_of_row_eq
plain-language theorem explainer
If two finite edge-kernel operators agree at every edge when acting on a fixed edge perturbation, then the resulting edge perturbations are identical as maps. Gravity workers matching Regge TT Hessians to lattice Lichnerowicz stencils on the 5×5×5 Freudenthal torus cite this to promote pointwise row checks to operator equality. The proof is pure functional extensionality on the edge index.
Claim. Let $K_R$ and $K_L$ be finite edge-kernel matrices on the $5\times 5\times 5$ periodic Freudenthal edges, and let $\varepsilon$ be an edge perturbation. If for every edge $e$ one has $(K_R\varepsilon)(e)=(K_L\varepsilon)(e)$, then $K_R\varepsilon=K_L\varepsilon$ as maps from edges to $\mathbb{R}$.
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on the encoded periodic Freudenthal torus. The conformal (vertex-scalar) ansatz cannot carry pure shear or TT gravitational-wave modes, so independent edge-length perturbations are treated separately from vertex-conformal ones.
A PeriodicEdgeOperatorKernel5 is a real matrix indexed by pairs of edges of the canonical $5\times 5\times 5$ periodic complex: the concrete surface on which a Regge TT Hessian stencil and a lattice Lichnerowicz stencil are compared. An edge perturbation is simply a real assignment to each such edge. The operator application is the matrix-vector product $(K\varepsilon)(e)=\sum_f K(e,f),\varepsilon(f)$.
This lemma sits one step below entrywise kernel equality: it only needs the two operators to agree after acting on a single fixed $\varepsilon$, row by row.
proof idea
One-line functional-extensionality argument. Apply funext on the edge index $e$, then discharge each point by the given row-agreement hypothesis. No algebraic content about kernels or stencils is used.
why it matters
Feeds periodicEdgeKernelOperator5_eq_of_kernel_eq, which lifts full entrywise kernel equality to operator equality on every perturbation, and is consumed by the data structure PeriodicTTHessianLichnerowiczMatchData5 whose field matches_on_tt is the analytic target of the TT Hessian-to-Lichnerowicz comparison.
In the Recognition gravity track this is bookkeeping infrastructure for proving that the discrete spin-2 Lichnerowicz operator and the Regge second variation agree on transverse-traceless edge modes of the Freudenthal lattice. It does not itself establish any continuum GR limit or forcing-chain step (T0–T8); it only makes the finite-matrix comparison well-typed and usable downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.