deficitDirectionalDerivFromLocalAngles
plain-language theorem explainer
Assembles the directional derivative of a hinge deficit under a conformal vertex-potential deformation from local tetrahedral dihedral-angle derivatives. Cited by anyone proving Regge first variation or conformal Schläfli cancellation on a 3D triangulation. Definitional: negative sum of packaged local angle derivatives over tets incident to the edge, matching d(2π − Σθ) = −Σ dθ.
Claim. Given a 3D triangulation $K$, a package of local dihedral-angle directional derivatives under the conformal ansatz, a vertex potential $\eta$, and an edge $e$, return $-\sum_{\tau} \partial_\eta \theta_{\tau,f}$, summing over tetrahedra $\tau$ that contain $e$, where $f$ is the local edge-slot of $e$ in $\tau$ (summand $0$ if $e\notin\tau$). This is the candidate directional derivative of the deficit angle at $e$ along the conformal line through $\eta$.
background
The module targets vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric engine is Schläfli cancellation plus zero deficit; this file records the analytic statement and the named local inputs until the closed-form local Schläfli identities are fully expanded.
Deficit at a hinge is $2\pi-\sum\theta$. Under a conformal deformation driven by a vertex potential $\eta$ along the line $t\mapsto$ conformal edge lengths at $t\eta$, each local dihedral angle in each tetrahedron has a directional derivative at $t=0$. Those derivatives are packaged as a map sending $(\eta,\tau,f)$ to a real, together with a HasDerivAt certificate for every tet and every one of its six edge-slots.
This definition lifts the local cofactors to a single edge-indexed real by summing, with a global minus sign, over all tetrahedra that contain the given edge (via the triangulation's edge-in-tet incidence).
proof idea
Pure definitional assembly, not a proved identity. For each tetrahedron index $\tau$, query whether edge $e$ appears in $\tau$. If absent, contribute $0$; if present at local slot $f$, contribute the packaged local angle derivative at $(\eta,\tau,f)$. Negate the finite sum. The minus sign is forced by deficit $=2\pi-\sum\theta$: the constant drops under differentiation and the sum of angle derivatives flips sign. No lemmas are applied; the body is a match-and-sum over the triangulation's incidence data.
why it matters
Feeds deficitAngle_hasDerivAt_from_localAngles, which certifies that this real is the actual derivative of the deficit-angle function along the conformal line at $t=0$. That certificate is wrapped into the deficit derivative package and consumed by ConformalSchlaefliCancellation and ConformalSchlaefliIncidenceBookkeeping: the exact Schläfli cancellation needed by the conformal first variation once local dihedral directional derivatives exist.
Incidence bookkeeping then turns the edge-indexed deficit variation into a sum of local tetrahedral Schläfli sums. Downstream, the Gravity module's physical six-tet cubic Dirichlet instance uses the same assembly for canonical periodic deficit derivative packages on Freudenthal-torus triangulations. This is the analytic bridge from local angle derivatives to global first-variation vanishing of the nonlinear Regge action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.