PeriodicEdgePerturbation5
plain-language theorem explainer
Real-valued assignments to the edges of the N=5 periodic Freudenthal triangulation. Track 1.D tensor/shear work cites this as the ambient function space of independent edge-length (or log-strain) perturbations, distinct from vertex-conformal scalars. The declaration is a one-line type abbreviation: maps from the typed periodic edge set into the reals.
Claim. Let $E_5$ be the set of edges of the periodic Freudenthal triangulation with periods $(5,5,5)$. An edge perturbation is any real-valued map $\delta\ell : E_5 \to \mathbb{R}$.
background
Track 1.D opens the tensor/shear sector of the weak-field Regge analysis. Track 1.B already assigns one scalar potential per vertex and induces edge-length changes by averaging endpoint values; that conformal slice cannot represent pure shear, so it misses transverse-traceless gravitational-wave modes. This module therefore treats edge perturbations as independent data and separates them from vertex-conformal perturbations.
The domain is the typed edge set of the N=5 periodic Freudenthal torus (periods 5 along each lattice axis), written here as the abbreviation for PeriodicEdge 5 5 5. That finite edge index is the discrete 1-skeleton on which Regge edge lengths, first variations, and later TT projectors live. An edge perturbation is simply a real function on those edges: the ambient linear space before imposing conformal, gauge, or TT constraints.
proof idea
Definitional abbreviation only: the name is synonymous with the function type from the N=5 periodic edge set into $\mathbb{R}$. No proof obligations, lemmas, or tactics.
why it matters
This type is the carrier space for the entire Track 1.D handoff. Downstream master-theorem endpoints quantify over it: conformal-generator span (every conformal log-subspace element is a finite linear combination of vertex generators), TT orthogonal-surface and projector-data reductions, gauge-generator projector data, finite-generator projector reduction, and the Regge-TT Hessian / lattice Lichnerowicz bilinear match on longitudinal TT modes. Edge-tensor-sector lemmas also restate conformal-log subspace membership in terms of maps of this type. Without a single ambient edge-perturbation space, the conformal/gauge/TT decomposition targets and the shear-versus-conformal rectangle obstruction cannot be stated uniformly on the N=5 torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.