encodedToPeriodicEdgePerturbation5
plain-language theorem explainer
Transports an edge-length perturbation from the encoded finite triangulation of the 5×5×5 periodic Freudenthal torus onto the typed periodic edge set. Anyone comparing the conformal log-strain slice to the full edge-perturbation space in Track 1.D cites this reindexing. The body is a one-line pullback along the inverse of the canonical edge equivalence.
Claim. Given an edge perturbation $\varepsilon$ indexed by the encoded edges of the canonical $5\times 5\times 5$ periodic Freudenthal torus, define the typed periodic edge perturbation by $(\varepsilon_{\mathrm{per}})(e)=\varepsilon(\iota^{-1}(e))$, where $\iota$ is the canonical equivalence from typed periodic edges to encoded finite edges.
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on a discrete complex. The Track 1.B conformal ansatz puts one scalar potential at each vertex and induces edge-length variations by averaging the two endpoint potentials. That scalar slice cannot represent pure shear, so it cannot cover transverse-traceless gravitational-wave modes. This module therefore treats independent edge perturbations as primary data and studies which of them arise from vertex potentials.
Two indexings of the same edge set appear. Typed periodic edges are the geometric edges of the periodic Freudenthal torus (pairs of lattice vertices with the usual Freudenthal incidence). Encoded edges are the finite combinatorial edges of the canonical encoded complex PeriodicTorus5 (the $5\times 5\times 5$ torus). An edge perturbation is simply a real-valued function on whichever edge set is in play.
The canonical edge equivalence of PeriodicTorus5 identifies the two indexings. The present map pulls an encoded perturbation back to the typed side by precomposition with the inverse equivalence.
proof idea
One-line definitional wrapper: send a typed periodic edge $e$ to the value of the encoded perturbation at the preimage of $e$ under the torus edge equivalence. No lemmas are applied; the body is pure reindexing.
why it matters
This transport is the bridge between the encoded finite complex (where vertex potentials, conformal log-strain, and the conformal predicate live) and the typed periodic edge language used by the conformal subspace and its generators. Downstream, the periodic conformal log-strain subspace is defined as the image of encoded conformal log-strain under this map; the unit vertex-delta conformal generators are built by applying it to encoded conformal strains; and the equivalence between typed and encoded conformal predicates factors through the same reindexing (and its inverse). Without it, the rectangle obstruction and the shear-versus-conformal split cannot be stated uniformly on both sides of the encoding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.