localDeficitAngleContribution_hasDerivAt_from_localAngles
plain-language theorem explainer
Along a conformal line of vertex potentials, each local incidence contribution to an edge deficit is differentiable at the flat point. The derivative is zero when the edge misses the tetrahedron, and otherwise equals the packaged local dihedral directional derivative. Anyone assembling the first variation of the nonlinear Regge action cites this. The proof is a two-branch case split on incidence, reducing to a constant derivative or the package axiom.
Claim. Let $K$ be a 3D triangulation and $A$ a package of local dihedral directional derivatives under the conformal ansatz. For any vertex potential $\eta$, global edge $e$, and tetrahedron $\tau$, the map $t \mapsto$ (local incidence contribution of $\tau$ to the deficit at $e$ along the conformal line through $\eta$) is differentiable at $t=0$, with derivative $0$ if $e$ is not incident to $\tau$, and otherwise equal to $A$'s directional derivative of the corresponding local dihedral angle.
background
This module targets the 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; the analytic work is to differentiate edge lengths, dihedral angles, and deficit angles under a conformal vertex-potential ansatz.
A local deficit-angle contribution is the incidence term at a global edge $e$ from one tetrahedron $\tau$: if $e$ sits in $\tau$ at local slot $f$, it is the conformal dihedral angle of that slot; otherwise it is zero. The deficit angle itself is assembled by summing these local contributions (and subtracting from $2\pi$ in the usual way downstream).
The structure LocalDihedralDirectionalDerivativePackage packages, for each tet and local edge slot, both the claimed directional derivative value and the HasDerivAt fact for the conformal dihedral angle along the line potential $t \mapsto \eta + t\cdot\mathbf{1}$-style deformation at $t=0$. Incidence is read off $K$.edgeInTet.
proof idea
Unfold the local contribution definition, which is a match on $K$.edgeInTet $e$ $\tau$.
- If the match is
none(edge not in the tet), the contribution is the constant zero function of $t$. ApplyhasDerivAt_constand simplify with the match hypothesis. - If the match is
some f, the contribution is exactly the conformal dihedral angle of slot $f$ on tet $\tau$ along the line potential. Invoke the package fieldA.angle_hasDerivAt$\eta$ $\tau$ $f$, and simplify with the match hypothesis.
No further calculus: the package already supplies the local angle derivative.
why it matters
This is the per-tetrahedron brick for differentiating deficit angles. The immediate parent is deficitAngle_hasDerivAt_from_localAngles, which sums local contributions (via the packaged local derivatives) to obtain HasDerivAt for the full edge deficit along the conformal line.
That deficit derivative is an essential input to the module's target: vanishing of the first variation of the nonlinear Regge action at the flat conformal potential, via Schläfli cancellation plus zero deficit. Until closed-form local Schläfli identities are fully expanded into derivative calculations, the package is the named analytic interface this lemma consumes and the deficit lemma propagates.
In the broader Recognition geometry stack, controlled first variation of discrete curvature under conformal deformations is the bridge from triangulation data toward continuum Einstein-Hilbert behaviour; this lemma keeps that chain honest at the incidence level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.