EncodedEdgeOperatorKernel5
plain-language theorem explainer
Type alias for real edge-to-edge operator matrices on the encoded 5×5×5 periodic Freudenthal torus, indexed by Fin nE. Anyone comparing Regge Hessian kernels to lattice Lichnerowicz kernels in the Track 1.D shear sector cites this surface. The body is a pure type abbreviation, not a proved claim.
Claim. An encoded edge-operator kernel on the canonical $5\times 5\times 5$ periodic Freudenthal torus is a real bilinear form on the finite set of edge indices: a map $\mathrm{Fin}\,n_E\times\mathrm{Fin}\,n_E\to\mathbb{R}$, where $n_E$ is the number of edges in that triangulation.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. The older conformal ansatz puts one scalar at each vertex and averages endpoint values onto edges; that slice cannot carry pure shear or transverse-traceless gravitational-wave modes. This module therefore treats independent edge-length perturbations separately from vertex-conformal ones.
The working lattice is the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus. Edges are enumerated by a finite index set $\mathrm{Fin},n_E$ coming from that encoding. An edge-operator kernel is simply a real matrix on that index set: the native surface on which numerically or symbolically extracted Regge and Lichnerowicz operators are stored before they are pulled back to typed periodic-edge indices.
Upstream, the torus abbreviation fixes the triangulation size and the edge-count constant $n_E$; the dimensionless bridge ratio $K=\varphi^{1/2}$ appears only as part of the broader constant stack and is not used in the type itself.
proof idea
No proof. The declaration is a one-line type abbreviation equating the name to the function type $\mathrm{Fin},n_E\to\mathrm{Fin},n_E\to\mathbb{R}$ on the edge count of the $5\times 5\times 5$ periodic torus. There are no tactics, lemmas, or obligations.
why it matters
This type is the shared carrier for every encoded-edge residual and certificate in the shear track. Downstream, the residual kernel is the pointwise difference of two such matrices (Regge minus Lichnerowicz); a pullback map sends an encoded kernel to a typed periodic-edge kernel via the torus edge equivalence. Four coefficient-data structures for the TT Hessian/Lichnerowicz residual (origin-column and relative/translated variants) store a pair of these kernels plus generator coefficient rows, then prove scalar formulas against the generator map.
In the Recognition gravity program this is scaffolding for matching discrete Regge second variation to continuum Lichnerowicz action on pure shear modes, the piece the conformal Track 1.B ansatz cannot reach. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is lattice infrastructure for the weak-field tensor sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.