deficitLineDeriv_zero_eq_deficitPackage
plain-language theorem explainer
At the flat point (parameter zero), the line derivative of the Regge deficit angle equals the first-variation deficit derivative carried by a deficit package. Anyone wiring a first-variation package into the nonlinear Regge Hessian cites this identification. The proof unfolds the line-derivative definition and extracts the unique derivative from the package's HasDerivAt witness.
Claim. Let $K$ be an incidence-consistent 3D triangulation, $D$ a deficit-angle directional-derivative package on $K$, $\xi$ a vertex potential, and $e$ an edge. Then the ordinary derivative at $s=0$ of $s\mapsto\delta_e(K,\gamma_\xi(s))$ (deficit angle of $e$ along the line potential through $\xi$) equals the package value $D_{\mathrm{def}}(\xi,e)$.
background
This module isolates the remaining hard step for the full nonlinear Regge action: the second directional derivative of the action at the flat potential must match the canonical incidence Hessian. Once that chain-rule calculation is in hand, the existing second-variation input structure follows at once.
A deficit-angle directional-derivative package packages, for every vertex potential and edge, a real number together with a HasDerivAt witness that this number is the derivative of the edge deficit angle under the line deformation of the potential. The line derivative deficitLineDeriv is the ordinary real derivative (via Mathlib deriv) of that same path, evaluated at a real parameter $s$.
The flat configuration is $s=0$: the line potential collapses to the base potential, so the two presentations of the first variation must agree there before any second-variation or mixed hinge/deficit identity can be stated without opaque deriv wrappers.
proof idea
Unfold the definition of the line derivative. From the package, obtain the HasDerivAt witness that the map $s\mapsto$ deficit angle of $e$ along the line potential through $\xi$ has derivative equal to the package's deficit derivative at $s=0$. A one-step convert aligns the function bodies, then HasDerivAt.deriv extracts the equality of the Mathlib deriv value with the package number.
why it matters
This is a small but necessary bridge inside the nonlinear Regge Hessian proof interface. Downstream, mixedHingeDeficitCanonicalHessian_of_deficitPackage consumes a deficit package plus a mixed hinge/deficit target stated in package form, and discharges the canonical mixed hinge/deficit Hessian target. The companion doc notes that the package form "removes the opaque deriv wrappers" and "exposes the exact first-variation deficit derivative that must be identified with the canonical Hessian."
Without equating the line derivative at zero to the package field, that rephrasing cannot start. In the broader Recognition geometry stack this sits under the second-variation chain that feeds ReggeActionSecondVariationInput: matching the nonlinear second directional derivative at the flat potential to the canonical incidence Hessian. It is bookkeeping relative to T8 ($D=3$) triangulation geometry, not a new physical assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.