conformalEdgeLogStrain
plain-language theorem explainer
Maps a scalar vertex potential on a 3D triangulation to the induced first-order log-length strain on edges by averaging the two endpoint values. Gravity and Regge-calculus workers cite it as the concrete conformal ansatz that Track 1.B lives inside. The body is a one-line endpoint average, not a derived identity.
Claim. Given a 3D triangulation $K$ and a real scalar potential $\xi$ on its vertices, define an edge perturbation by sending each edge $e$ with endpoints $u,v$ to $(\xi(u)+\xi(v))/2$. This is the first-order log-length strain of the vertex-conformal ansatz.
background
Track 1.D isolates the tensor/shear sector of weak-field Regge gravity. Track 1.B already assigns one scalar potential per vertex and induces edge-length variations by averaging endpoints; that scalar slice cannot represent pure shear or transverse-traceless gravitational-wave modes. This module therefore separates free edge perturbations from the conformal image.
An edge perturbation is a real assignment to each global edge of $K$ (one degree of freedom per edge), the natural finite Regge surface for anisotropic shear and TT modes. A vertex potential is the dual scalar field on vertices. The conformal ansatz is the map that turns the latter into the former by endpoint averaging; the companion length perturbation multiplies that log-strain by the background edge length scale $\sqrt{\ell_e^2}$.
Upstream geometry supplies the triangulation edge-endpoint map and the linearized deficit machinery; the present definition only packages the conformal strain itself.
proof idea
Definitional, not a proof. For each edge $e$, read the ordered endpoint pair from the triangulation's edge-vertex table and return the arithmetic mean of the two vertex-potential values. No lemmas are applied; the term is the pure endpoint average that later theorems treat as the generator of the conformal subspace.
why it matters
This is the concrete realization of the Track 1.B conformal ansatz inside the tensor/shear scaffold. Downstream, IsConformalEdgePerturbation is exactly membership in its image, and the SevenGaps edge-tensor sector packages it as an $\mathbb{R}$-linear map from vertex potentials to edge perturbations. The identity relating conformal length perturbation to $\sqrt{\ell_e^2}$ times this log-strain is definitional from it.
It feeds the rectangle obstruction: opposite edges of a quadrilateral forced to equal conformal log-strain cannot carry nontrivial pure shear. Periodic generators on the five-edge torus are built by applying it to encoded vertex-delta potentials, so the conformal subspace used in the seven-gaps analysis is literally its range. Framework-wise it sits in the gravity track that must eventually separate conformal modes from the TT shear needed for gravitational waves; it does not itself force $D=3$ or the eight-tick structure, but it is the scalar slice those later comparisons subtract against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.