conformalLocalSqEdge
plain-language theorem explainer
Local squared-edge length of tetrahedron τ under a vertex-conformal potential ξ. Edge f with endpoints (u,v) is rescaled by exp(ξ_u + ξ_v) against the background squared length. Anyone differentiating the Regge action or assembling Cayley–Menger edge data under the conformal ansatz cites this. The body is a pure definition: look up the edge's two vertices and multiply by the exponential factor.
Claim. For a finite 3D triangulation $K$, vertex conformal potential $\xi$, tetrahedron index $\tau$, and local edge index $f\in\{0,\ldots,5\}$ with endpoints $(u,v)$ in the tetrahedron, the conformally scaled squared edge length is $(K.\mathrm{tet}\,\tau).\ell_f^2 \cdot \exp(\xi_u+\xi_v)$.
background
The module isolates the analytic Hessian of the Regge action on a finite 3D triangulation under the conformal ansatz, packaging it into the existing ReggeHessianData interface. A vertex conformal potential is a real assignment to each vertex of $K$; the zero potential recovers the background metric.
Edges of a tetrahedron are indexed by $\mathrm{Fin},6$, with the standard pairing edge $0=(0,1)$, $1=(0,2)$, $2=(0,3)$, $3=(1,2)$, $4=(1,3)$, $5=(2,3)$. The background squared edge lengths live on each tetrahedron; the conformal ansatz multiplies the edge joining $u$ and $v$ by $\exp(\xi_u+\xi_v)$, which is the discrete analogue of $g\mapsto e^{2\phi}g$ at the level of edge lengths squared.
Upstream, edgeVertices supplies the $(u,v)$ lookup, and VertexPotential is just $\mathrm{Fin},n_V\to\mathbb{R}$.
proof idea
Definitional, not a proof. Resolve the local edge index $f$ to its two tetrahedron-local vertices via the fixed edge-to-vertex table, map those to global vertex indices through the tetrahedron's vertex list, evaluate $\xi$ at both endpoints, and return background squared length times $\exp(\xi_u+\xi_v)$.
why it matters
This is the atomic edge datum for the whole conformal Regge package. It is wrapped immediately into the six-edge Cayley–Menger tuple for each tetrahedron, and then into dihedral angles, deficit angles, hinge measures, and the full Regge action under the conformal line.
Downstream first-variation work differentiates it along the conformal line at $t=0$; the nonlinear Hessian proofs use positivity of the scaled edges, expand global Schläfli sums into local tetrahedral contributions, and feed the second-variation target that closes the concrete Hessian step. In the Recognition geometry stack this is the discrete conformal deformation used to probe the Regge Hessian on 3D triangulations (the $D=3$ setting forced upstream).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.