encodedToPeriodicEdgeKernel5
plain-language theorem explainer
Converts an edge-operator kernel written on raw Fin indices of the 5×5×5 Freudenthal torus into the same kernel on typed periodic edges. Gravity Track 1.D uses this whenever a numerically extracted stencil must sit on the typed matrix surface where Regge TT Hessians and lattice Lichnerowicz operators are compared. The body is a one-line pullback along the edge-index equivalence.
Claim. Given a real matrix $K$ indexed by $\mathrm{Fin}\, n_E$ (the encoded edge set of the canonical $5\times 5\times 5$ periodic Freudenthal torus), define the pulled-back matrix $\widetilde{K}$ on typed periodic edges by $\widetilde{K}(e,f) = K(\iota^{-1}(e),\iota^{-1}(f))$, where $\iota$ is the edge-index equivalence of that torus.
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on a discrete triangulation. The conformal (vertex-scalar) ansatz of Track 1.B cannot carry pure shear, so independent edge-length perturbations are needed to reach transverse-traceless modes.
Two matrix surfaces appear. EncodedEdgeOperatorKernel5 is the native Fin-indexed kernel extracted from the encoded Freudenthal triangulation. PeriodicEdgeOperatorKernel5 is the typed edge-to-edge matrix on which the Regge TT Hessian stencil and the lattice Lichnerowicz stencil are compared. PeriodicTorus5 is the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus supplying the edge equivalence between those index sets.
This definition is the pure reindexing map that moves a kernel from the encoded Fin surface onto the typed periodic-edge surface.
proof idea
One-line definitional pullback: apply the input Fin-kernel at the preimages of the two typed edges under PeriodicTorus5.edgeEquiv.symm. No lemmas are invoked; the body is the lambda that performs that double preimage.
why it matters
Downstream, the apply lemma records definitional equality of the pullback, and two residual-data structures for the TT Hessian-to-Lichnerowicz comparison store kernels of typed type PeriodicEdgeOperatorKernel5. Those structures target residual vanishing on TT perturbations and the entrywise residual formula (Regge kernel minus Lichnerowicz kernel equals the generator-map reconstruction). Without this reindexing, numerically extracted Fin-kernels cannot sit on the comparison surface. The declaration is scaffolding glue inside Track 1.D, not a forcing-chain step; it enables the finite TT residual calculations that test whether discrete shear matches continuum Lichnerowicz behavior on the periodic torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.