PeriodicEdgeOperatorKernel5
plain-language theorem explainer
A finite real matrix indexed by pairs of edges on the period-5 Freudenthal torus, representing linear operators on edge-length perturbations. Gravity and discrete-geometry workers cite it as the common surface on which the Regge transverse-traceless Hessian stencil and the lattice Lichnerowicz stencil are compared entrywise. It is a pure type abbreviation, not a proved identity.
Claim. Write $\mathrm{PeriodicEdgeOperatorKernel}_5$ for the type of maps $E_5\times E_5\to\mathbb{R}$, where $E_5$ is the finite set of edges of the period-5 periodic Freudenthal triangulation. Such a map is the matrix of a linear operator acting on real edge perturbations.
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on a discrete triangulation. The older conformal ansatz puts one scalar at each vertex and averages to edges; that slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. Independent edge perturbations are therefore treated as the primary variables.
The ambient complex is the period-5 periodic Freudenthal torus (imported from the geometry layer). Its edges form a finite typed index set. An operator on edge perturbations is then just a real matrix with those edge indices: the present abbreviation names that matrix type.
The dimensionless bridge ratio $K=\varphi^{1/2}$ appears in the encoded finite-index surface that feeds this typed kernel; the comparison target is the continuum Lichnerowicz operator discretized on the same lattice.
proof idea
No proof. The declaration is a one-line type abbreviation equating the name to the function type from pairs of period-5 edges into the reals. Downstream code treats values of this type as kernel matrices and builds the associated linear maps by finite summation over edges.
why it matters
This type is the shared matrix surface on which the Regge TT Hessian stencil and the lattice Lichnerowicz stencil are meant to agree. Downstream definitions pull encoded $\mathrm{Fin},n_E$ kernels onto typed periodic edges, apply a kernel as an operator on edge perturbations, extract rows as edge vectors, form residual kernels, and prove that entrywise or rowwise kernel equality implies operator equality. Those lemmas are the concrete comparison machinery for the tensor/shear track: without a common finite kernel type, stencil identity cannot even be stated. In the broader Recognition scaffold this sits under discrete gravity on the eight-tick / finite-register side, not under the T5–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.