directionalFirstVariationFormula_of_deficitPackage
plain-language theorem explainer
Given a 3D triangulation and a package of directional derivatives of deficit angles that obey global Schläfli cancellation, the first derivative of the nonlinear Regge action along every conformal line through the flat potential equals the sum of hinge-measure derivatives times the flat deficits. Discrete-gravity and Regge-calculus workers cite this as the analytic product-rule form of the first variation. The proof multiplies hinge and deficit derivatives edgewise, sums, then cancels the Schläfli term.
Claim. Let $K$ be an incidence-consistent 3D triangulation. Suppose one is given, for every conformal direction $\eta$ and every edge $e$, a directional derivative of the deficit angle at the flat potential, such that the sum over edges of (hinge measure at flat) times (that deficit derivative) vanishes (global Schläfli cancellation). Then for every $\eta$, the map $t \mapsto S_{\mathrm{Regge}}(\phi_0 + t\eta)$ is differentiable at $t=0$ with derivative $\sum_e (\partial_\eta \ell_e)\,\delta_e(\phi_0)$, where $\ell_e$ is the hinge measure and $\delta_e$ the deficit.
background
This module treats the first variation of the full nonlinear Regge action on a 3D triangulation $K$. The action is the sum over edges of hinge measure times deficit angle. Configurations are conformal vertex potentials; the flat background is the zero potential. Lines through flat are $t \mapsto$ linePotential$(\eta,t)$.
The structure DeficitAngleDirectionalDerivativePackage packages, for each direction $\eta$ and edge $e$, a real number claimed to be the $t$-derivative at $0$ of the deficit along that line, together with the identity that the weighted sum of those derivatives against the flat hinge measures vanishes. That identity is exactly global Schläfli cancellation in the conformal direction.
The target structure ReggeActionDirectionalFirstVariationFormula asserts the one-variable product-rule form: the derivative of the Regge action along every such line equals $\sum_e$ (hinge-measure directional derivative) times (flat deficit). Spatial dimension $D=3$ is the ambient setting forced by the Recognition chain (T8).
proof idea
Fix a direction $\eta$. For each edge, the product rule on (hinge measure along the line) times (deficit along the line) yields a derivative at $0$ equal to hingeDeriv$\cdot$flatDeficit $+$ flatHinge$\cdot$deficitDeriv, using the package's deficit_hasDerivAt and the already-proved hinge-measure line derivative.
Sum those edgewise derivatives via HasDerivAt.sum. The summed second summand is exactly the package's schlaefli_cancellation field, hence vanishes. After rewriting the target sum, the remaining derivative is $\sum_e$ hingeDeriv$\cdot$flatDeficit, which is the claimed directional formula. A final convert/ext/simp matches the unfolded Regge action to the summed product.
why it matters
The module's stated target is vanishing of the first variation of the nonlinear Regge action at the flat conformal potential, by Schläfli cancellation plus zero deficit. This theorem supplies the intermediate analytic identity: the directional derivative equals the hinge-weighted flat-deficit sum, once a deficit-derivative package with Schläfli cancellation is in hand.
It is consumed by reggeActionFirstVariationInput_of_localAngles, which assembles the full first-variation input from local dihedral packages and a conformal Schläfli hypothesis. That is the bridge from closed-form local Schläfli identities to the global variation statement.
In the Recognition geometry stack this sits under $D=3$ (T8) discrete gravity: Regge calculus on triangulations is the natural discrete Einstein-Hilbert action. The result does not yet force the variation to zero; zero deficit at flat is a separate input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.