deficitLineDeriv
plain-language theorem explainer
Directional derivative of the Regge deficit angle at a fixed global edge, taken along the conformal ray through a vertex potential. Anyone expanding the first variation of the conformal Regge action into hinge-length times deficit-rate factors cites this. It is a one-line definition: the ordinary real derivative of the deficit along that ray.
Claim. Fix a 3D triangulation $K$, a vertex potential $\xi$, a global edge $e$, and a real parameter $t$. Write $\xi_s$ for the conformal line potential $i\mapsto s\,\xi_i$. The deficit-line derivative at $t$ is $\frac{d}{ds}\big|_{s=t}\delta_e(\xi_s)$, where $\delta_e$ is the Regge deficit angle of $e$ under the conformal ansatz.
background
The ambient module isolates the remaining hard step of the nonlinear Regge Hessian: the second directional derivative of the conformal Regge action at the flat potential must match the canonical incidence Hessian. Once that chain-rule calculation is filled, the existing second-variation input package follows at once.
Under the conformal ansatz the deficit at a global edge is $\delta_e(\xi)=2\pi-\sum_\tau\theta_{e,\tau}(\xi)$, the usual $2\pi$ minus the sum of local dihedral contributions from incident tetrahedra. The conformal line through the flat configuration in direction $\xi$ is the one-parameter family of vertex potentials $s\mapsto s\cdot\xi$ (each vertex scaled by the same real factor $s$).
The first variation of the Regge action along that line splits into a weighted sum of hinge-length rates and deficit rates. This definition packages the deficit-rate factor as an ordinary one-variable derivative, so later Schläfli and product-rule targets can name it cleanly.
proof idea
Pure definition, not a proved identity. The body applies Lean's deriv to the composite $s\mapsto\delta_e(\xi_s)$, where $\delta_e$ is the concrete conformal deficit angle and $\xi_s$ is the conformal line potential. No lemmas are invoked; explicit local cofactor or arccos differentiation is deferred to downstream targets that expand this quantity near the flat point.
why it matters
This is the named deficit-rate factor in every conformal Schläfli target in the module. The strongest geometric form asserts that $\sum_e h_e(\xi_t),\delta'_e(t)=0$ for every $t$ (classical Schläfli summed over tetrahedra), which cancels the $\sum h\delta'$ term in the first variation and leaves $S'(t)=\sum\delta,h'$. Near-flat expansion targets rewrite the same weighted sum as local tetrahedral Schläfli sums by expanding this derivative as minus the sum of local angle derivatives and matching global hinge lengths to local edge slots.
It also feeds the product-rule target for the action derivative near zero, the differentiability-at-zero lemma under a flat configuration, and the identification of the value at zero with the packaged first-variation deficit term. In the Recognition geometry stack this is bookkeeping on the way to the nonlinear directional Hessian equaling the canonical incidence form, not a new physical postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.