periodicToEncodedEdgePerturbation5
plain-language theorem explainer
Maps an edge-length perturbation on the typed N=5 periodic Freudenthal edges to the same data on encoded Fin nE indices by precomposing with the torus edge equivalence. Gravity and Regge-calculus workers cite it whenever a typed shear or strain must be stated in the census/encoded edge basis. The body is a one-line function composition.
Claim. Given an edge perturbation $\varepsilon$ on the typed periodic edges of the $N=5$ Freudenthal torus, define the encoded perturbation by $(\varepsilon^{\mathrm{enc}})(e) = \varepsilon(\iota(e))$, where $\iota$ is the canonical bijection from encoded finite edge indices to typed periodic edges.
background
Track 1.D opens the tensor/shear sector of weak-field gravity on the Recognition lattice. Track 1.B only supplies a vertex-scalar conformal ansatz (one potential per vertex, edge strains by endpoint averaging). That slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module therefore treats independent edge-length perturbations as the ambient space and isolates the conformal subspace inside it.
Two coordinate systems are used for the $N=5$ periodic Freudenthal torus. Typed periodic edges (PeriodicEdge5) are the geometric objects; encoded edges are finite indices Fin nE for the triangulation census. A typed perturbation is a real function on typed edges; an encoded perturbation is the same data on Fin nE. The bridge constant $K=\varphi^{1/2}$ enters only as the triangulation parameter package, not in the map itself.
The map is the push along the fixed edge equivalence of PeriodicTorus5: evaluate the typed function at the typed edge corresponding to each encoded index.
proof idea
Definitional one-liner. On an encoded edge $e$, return the typed perturbation evaluated at PeriodicTorus5.edgeEquiv e. No lemmas are invoked; the term is pure function composition. The inverse direction (encoded to typed) is the sibling pullback, and together they form the equivalence used downstream.
why it matters
This is the forward half of the typed/encoded dictionary for the $N=5$ tensor/shear surface. It is the invFun of periodicEdgePerturbationEquiv5, which asserts the two views are exactly equivalent, and it is how periodicRawSplittingOfEncoded5 carries conformal/shear splittings across that equivalence.
In the SevenGaps edge-tensor sector it is the transport used to state conformal predicates and explicit counterexamples in encoded form: the typed/encoded conformal-slice equivalence, the encoded rectangle face shear, and the encoded uniform $x$-strain non-conformality all apply it. Those deliverables show that pure shear exists outside the vertex-conformal ansatz, which is the elementary obstruction needed before a Regge TT (transverse-traceless) sector can be built on the eight-tick, $D=3$ lattice.
It does not itself prove non-conformality or construct GW modes; it only standardizes the edge basis so those statements can be written once and reused.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.