localDeficitAngleContribution
plain-language theorem explainer
Local incidence term for the Regge deficit at a global edge under the conformal ansatz: the dihedral angle of tet τ at edge e if they meet, otherwise zero. Anyone assembling deficitAngle or differentiating the action cites it. The body is a one-line match on the triangulation incidence map.
Claim. Given a finite 3D triangulation $K$, a vertex potential $\xi$, a global edge $e$, and a tetrahedron $\tau$, the local deficit contribution is the conformal dihedral angle of $\tau$ at the local edge slot of $e$ when $e$ lies in $\tau$, and $0$ otherwise.
background
The module builds a concrete Regge action under a vertex-conformal ansatz on a finite 3D triangulation, then packages its second variation into the existing Hessian interface. Edges and tets are indexed finitely; a vertex potential $\xi$ scales squared edge lengths conformally at vertices.
Incidence is read from edgeInTet: for each global edge $e$ and tet $\tau$ one gets either a local edge slot $f\in{0,\ldots,5}$ or none. The dihedral angle of a tet edge under the ansatz is computed from the Cayley–Menger cofactor formula on the six conformal squared lengths of that tet.
Classically the hinge deficit is $2\pi$ minus the sum of dihedral angles around the edge. This definition isolates one tet’s term in that sum (or zero if the tet does not contain the edge).
proof idea
Pure definition by case split on incidence. Match K.edgeInTet e τ: on some f, return the conformal dihedral angle of tet $\tau$ at local slot $f$; on none, return $0$. No lemmas or tactics.
why it matters
This is the atomic summand of the global conformal deficit: deficitAngle is exactly $2\pi$ minus the sum of these contributions over all tets. First-variation theorems differentiate the local term and then the sum; smoothness at the flat point is proved first locally then globally. Nonlinear Hessian work equates the line derivative of the deficit to minus the sum of local derivatives near zero. Gravity preflight reuses the same conformal dihedral data. In the RS geometry stack this is the hinge curvature input to the concrete Regge action whose Hessian is the analytic target of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.