encodedToPeriodicEdgeKernel5_apply
plain-language theorem explainer
Evaluating a pulled-back edge operator kernel on typed periodic edges of the 5×5×5 Freudenthal torus equals evaluating the encoded Fin-index kernel on the inverse edge-equivalence images. Anyone wiring finite-triangulation kernels into typed periodic-edge operators cites this. The proof is definitional reflexivity.
Claim. For any encoded edge-operator kernel $K$ on the $5\times 5\times 5$ periodic Freudenthal torus (a real matrix indexed by $\mathrm{Fin}\,n_E$) and any two typed periodic edges $e,f$, the pullback kernel satisfies $\widetilde{K}(e,f)=K(\iota^{-1}(e),\iota^{-1}(f))$, where $\iota$ is the edge equivalence between encoded finite indices and typed periodic edges.
background
Track 1.D builds the tensor/shear sector missing from the Track 1.B conformal ansatz. Vertex-scalar potentials induce only averaged endpoint edge strains and cannot represent pure shear, so they miss transverse-traceless weak-field modes. This module separates independent edge perturbations from vertex-conformal ones on a fixed periodic triangulation.
The working geometry is the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus. Typed periodic edges (PeriodicEdge 5 5 5) are identified with the native finite edge-index set $\mathrm{Fin},K.nE$ via an edge equivalence. An encoded edge-operator kernel is simply a real bilinear form on that $\mathrm{Fin}$ surface; the pullback definition reindexes it to typed edges by applying the inverse equivalence on each argument.
The BIT and ILG kernel families supply continuum-style radial profiles elsewhere; here the object is the discrete edge-to-edge matrix extracted from the encoded triangulation, not a continuum kernel evaluation.
proof idea
One-line definitional proof: rfl. The pullback is defined by exactly the right-hand side, so equality of the two applications is judgmental.
why it matters
This lemma is the apply-form of the reindexing bridge between the encoded finite edge surface used by payload generators and the typed periodic-edge language used by the shear-sector operators. Without it, every later identity that mixes stencil coefficients, hinge-aware zero modes, or Freudenthal axis certificates with typed edges would have to unfold the pullback by hand.
It sits inside the Track 1.D scaffold that aims to cover pure shear and eventually TT gravitational-wave modes on the Regge side, complementary to the conformal vertex ansatz of Track 1.B. No downstream theorem yet consumes it (used_by is empty), so it is infrastructure for forthcoming kernel identities rather than a closed forcing-chain step. It does not touch T0–T8, RCL, or the mass ladder; its role is local discrete-geometry bookkeeping for the gravity track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.