conformalTetSqEdges
plain-language theorem explainer
Packages the six squared edge lengths of one tetrahedron under the vertex-conformal ansatz: each bare edge scales by exp(ξ_u+ξ_v). Cited by anyone differentiating dihedral angles or the Regge action along conformal lines. One-line pointwise wrapper around the local edge scaling map.
Claim. Given a finite 3D triangulation $K$, a real vertex potential $\xi$, and a tetrahedron index $\tau$, return the squared-edge data $f \mapsto \ell_f^2(\tau)\,\exp(\xi_u+\xi_v)$ for the six local edges $f$ of $\tau$, as a map $\mathrm{Fin}\,6\to\mathbb{R}$.
background
The module builds a concrete Regge action under a conformal ansatz on a finite 3D triangulation and feeds its second variation into the existing Hessian interface. Squared-edge data for a tetrahedron are six real numbers indexed by $\mathrm{Fin},6$ (the Cayley–Menger edge slots).
A vertex potential $\xi$ assigns a real number to each vertex. Under the conformal ansatz, a local edge with endpoints $u,v$ in tetrahedron $\tau$ has squared length scaled by $\exp(\xi_u+\xi_v)$. The sibling map that does this for one edge is the local conformal squared-edge formula; the present definition simply collects all six edges of $\tau$ into one squared-edge vector.
That vector is the natural input to the Cayley–Menger cofactor formulas for volume and dihedral angles used throughout the Regge calculus development.
proof idea
Definitional one-liner: the squared-edge map is $\lambda f.,\mathrm{conformalLocalSqEdge}(K,\xi,\tau,f)$. No proof obligations; it is pure packaging of the per-edge conformal scale into a $\mathrm{Fin},6\to\mathbb{R}$ object.
why it matters
This is the squared-edge input that every conformal dihedral and deficit computation in the concrete Regge package reads. Immediately downstream, the local dihedral angle under the conformal ansatz is the Cayley–Menger dihedral cosine applied to this map. First-variation work differentiates the package along the line potential through the origin, and the nonlinear Hessian proofs use it for positivity of the Cayley–Menger volume form near $t=0$, endpoint-free dihedral cosines, and the local Schläfli chain-rule package on flat configurations.
In the broader Recognition geometry stack it is scaffolding for the analytic Hessian of the 3D Regge action under conformal deformations (the module's stated target), not a forcing-chain landmark itself. It does not touch T5–T8 or the Recognition Composition Law; it is pure discrete-geometry infrastructure for the curvature side of the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.