deficitAngle
plain-language theorem explainer
Defines the Regge deficit angle at a global edge of a finite 3D triangulation under the vertex-conformal ansatz: $2\pi$ minus the sum of incident dihedral angles. Anyone writing the concrete Regge action, its first variation, or discrete Bianchi/Schläfli identities cites this. The body is a one-line sum over tetrahedra of the local incidence contributions.
Claim. For a finite 3D triangulation $K$, a vertex potential $\xi$, and a global edge $e$, the deficit angle is $\delta(K,\xi,e) := 2\pi - \sum_{\tau} \theta_{\mathrm{loc}}(K,\xi,e,\tau)$, where each local term is the conformal dihedral angle of tetrahedron $\tau$ at the face corresponding to $e$ when $e$ is incident to $\tau$, and $0$ otherwise.
background
The module builds a concrete 3D Regge action under a vertex-conformal ansatz and packages its Hessian into the existing Regge Hessian interface. Edges are the hinges; curvature is carried by deficit angles on those hinges.
A triangulation $K$ supplies finite edge and tetrahedron index sets. The vertex potential $\xi$ deforms edge lengths conformally. The sibling local contribution returns, for each tetrahedron $\tau$, either the dihedral angle of $\tau$ at the local face matching global edge $e$ (via the conformal dihedral map), or zero if $e$ does not meet $\tau$.
Classically, the deficit on a hinge is $2\pi$ minus the sum of dihedral angles of all tetrahedra around that hinge. This definition is exactly that sum, written edge-first over the whole triangulation.
proof idea
Pure definition, not a proved theorem. The right-hand side is $2\pi$ minus a finite sum, indexed by all tetrahedra of $K$, of the already-defined local incidence contributions. Each summand is either a conformal dihedral angle or zero according to the edge-in-tet incidence match; no further lemmas are applied in the body.
why it matters
This is the curvature scalar that multiplies hinge measure in the concrete Regge action: the action is $\sum_e \ell_e,\delta_e$. Downstream first-variation work differentiates this deficit in conformal directions and packages the global Schläfli cancellation. Discrete Bianchi and abstract Regge data treat deficit angles as bone holonomies; the four-tet star deficit uses the same $2\pi - \sum$ convention on a local star.
In the Recognition geometry track this supplies the discrete curvature input for the 3D Regge Hessian target ($D=3$ from the forcing chain). It does not itself force dimension or close the continuum limit; it is the hinge-level building block those arguments consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.