EdgePerturbation
plain-language theorem explainer
Edge-level first-order length perturbations on a finite 3D Regge triangulation: one real degree of freedom per global edge. Anyone working the tensor/shear or TT sector cites this as the ambient space of anisotropic strains, distinct from the vertex-conformal scalar slice. The declaration is a pure type abbreviation, Fin(nE) → ℝ.
Claim. For a finite 3D Regge triangulation $K$, an edge perturbation is a real-valued assignment to each global edge of $K$, i.e. a map $\eta : \{0,\ldots,n_E(K)-1\} \to \mathbb{R}$.
background
Track 1.D isolates the tensor/shear sector of weak-field Regge gravity. Track 1.B already has a conformal ansatz: one scalar potential per vertex, inducing edge-length changes by averaging the two endpoints. That scalar slice cannot carry pure shear, so it cannot represent transverse-traceless gravitational-wave modes.
A Triangulation3D packages abstract incidence data (vertex, edge, and tetrahedron counts, edge endpoints, tet vertex tuples) together with nondegenerate squared-edge data on each tetrahedron. The natural finite surface for anisotropic shear is then one free real per global edge, not per vertex.
Upstream, the geometry library already uses a closely related structure: a perturbation of flat edge-lengths as a map eta : Fin nE → ℝ, feeding linearized deficit angles and the Schläfli identity that makes the first-order Regge action vanish.
proof idea
No proof: the declaration is an abbreviation equating the name to the function type Fin K.nE → ℝ. It simply re-exports the edge-indexed real vector space already implicit in the triangulation's edge count.
why it matters
This type is the ambient space for the whole tensor/shear track. Downstream, the SevenGaps edge-tensor sector builds the vertex-conformal log-strain as a linear map into this space, proves its finite rank, and characterizes conformal edge perturbations as the range of that map. Geometry.DeficitLinearization uses the same edge-perturbation notion for linearized deficits and the certificate that the linear Regge action vanishes by Schläfli. The simplicial-ledger curvature certificate ultimately discharges against that linearization hypothesis.
In the Recognition framework this is scaffolding for covering TT modes that the conformal (vertex-potential) ansatz cannot reach, separating pure shear from the scalar slice before any continuum limit or eight-tick/octave timing is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.