periodicEdgePerturbationEquiv5
plain-language theorem explainer
On the N=5 periodic Freudenthal torus, edge-length perturbations indexed by encoded finite triangulation edges are canonically equivalent to those indexed by typed periodic edges. Regge and weak-field gravity workers cite this when moving between combinatorial edge labels and geometric edge types in the tensor/shear sector. The proof packages two conversion maps into an Equiv and checks both inverses by function extensionality and simplification.
Claim. There is a canonical equivalence between real-valued edge perturbations on the encoded finite edge set of the $N=5$ periodic triangulation and real-valued functions on the typed periodic Freudenthal edges of that same complex.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. Track 1.B's conformal ansatz places one scalar at each vertex and induces edge-length changes by averaging endpoint potentials; that slice cannot carry pure shear, so it cannot alone represent transverse-traceless gravitational-wave modes. This module therefore treats independent edge perturbations as primary data and separates them from vertex-conformal variations.
An edge perturbation is a real assignment to edges. For the $N=5$ periodic torus one has two presentations: the encoded view (functions on the finite triangulation edge index set of the complex) and the typed periodic view (functions on the named periodic Freudenthal edges). The module already defines the two conversion maps between these presentations; the present declaration packages them as a single equivalence.
Spatial dimension $D=3$ (forced at T8/T9) underlies the ambient lattice geometry, but the equivalence itself is purely combinatorial: it identifies two indexings of the same edge set.
proof idea
Definitional Equiv package, not a deep argument. Forward map is the existing pull from encoded finite edges to typed periodic edges; inverse is the reverse conversion. Left and right inverses are each proved by introducing an arbitrary perturbation, applying function extensionality on edges, and simplifying with the definitions of the two conversion maps. No external lemmas beyond those unfoldings are required.
why it matters
The Track 1.D scaffold endpoint theorem builds its second constructor component from this equivalence: it needs a concrete witness that the encoded and typed $N=5$ edge-perturbation surfaces are the same object. Without that identification, later predicates (conformal membership, gauge fixing, TT projection) would have to be stated twice, once per indexing.
In the broader Recognition gravity program this sits under the move from the pure conformal (scalar) ansatz to a genuine tensor/shear sector capable of hosting TT modes. It does not yet prove existence of nontrivial shear or TT zero modes; it only locks the two bookkeeping languages so those geometric claims can be stated once. Downstream scaffold closure for Track 1.D therefore depends on this definitional bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.