tetDihedralAngleUnderConformal
plain-language theorem explainer
Under a conformal vertex potential on a finite 3D Regge triangulation, this returns the dihedral angle at a chosen local edge of a tetrahedron from the six conformally scaled squared lengths. Anyone assembling deficit angles, first variations, or the conformal Schläfli expansion cites it. The body is a one-line composition of the Cayley–Menger arccos formula with the conformal squared-edge map.
Claim. Given a finite 3D triangulation $K$, a real vertex potential $\xi$, a tetrahedron index $\tau$, and a local edge index $f\in\{0,\ldots,5\}$, the value is the dihedral angle at that local edge of $\tau$ after conformal rescaling of all six squared edge lengths of $\tau$ by $\xi$, obtained as $\arccos$ of the Cayley–Menger cofactor cosine on those squared lengths.
background
The module builds a concrete Regge action and its second variation under the conformal ansatz on a finite 3D triangulation, then feeds the existing Hessian data interface. Geometry is discrete: lengths live on edges, curvature appears as angle deficits at hinges.
A vertex potential $\xi$ scales edge lengths conformally. For each tetrahedron $\tau$, the six squared edge coordinates are the conformally scaled local squared lengths. The dihedral angle on squared-edge data is $\arccos$ of the Cayley–Menger cofactor cosine for a chosen local edge among the six.
Upstream, the deficit at a hinge is $2\pi$ minus the sum of incident dihedral angles. This definition supplies each local angle that later enters that sum under the conformal deformation.
proof idea
One-line definitional wrapper: apply the squared-edge dihedral map to the six conformally scaled squared edges of tetrahedron $\tau$, at local edge $f$. No separate proof obligations; the meaning is entirely by composition of those two maps.
why it matters
This is the local angle primitive for the concrete conformal Regge package. The next definition uses it as the nonzero branch of a local incidence contribution to the global-edge deficit. First-variation structures package $\mathrm{HasDerivAt}$ along the conformal line potential for exactly this angle, in both length and squared-edge chain-rule forms, and the flat-configuration constructors discharge those packages by differentiating it at $t=0$.
Nonlinear Hessian work cites it inside the conformal Schläfli-along-line expansion target and the corresponding assembly lemma. In the Recognition geometry stack this is the explicit angle coordinate whose derivatives close the analytic Hessian step for 3D Regge under conformal deformations (the module’s stated goal), tying discrete curvature to the second variation of the action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.