DeficitAngleDirectionalDerivativePackage
plain-language theorem explainer
A data package that records directional derivatives of Regge deficit angles along conformal vertex-potential lines, together with the global Schläfli cancellation identity at the flat configuration. First-variation and nonlinear-correspondence theorems for the 3D Regge action take this package as named analytic input. As a structure it asserts no existence; constructors later discharge the fields from local dihedral derivatives.
Claim. For an incidence-consistent 3D triangulation $K$, a deficit-angle directional-derivative package consists of a map $\delta'$ sending each vertex potential $\eta$ and edge $e$ to a real number such that, for every $\eta$ and $e$, the map $t \mapsto$ (Regge deficit of $e$ along the line $t\eta$) is differentiable at $t=0$ with derivative $\delta'(\eta,e)$, and such that $\sum_e \ell_e(0)\,\delta'(\eta,e)=0$ for every $\eta$, where $\ell_e(0)$ is the conformal hinge measure (edge length) evaluated at the zero potential.
background
The module records the exact analytic input for the first variation of the nonlinear Regge action at the flat conformal potential. The geometric target is vanishing of that variation via Schläfli cancellation plus zero deficit; full closed-form derivative expansions are deferred to named packages of this kind.
The Regge deficit angle at a global edge is $2\pi$ minus the sum of local dihedral contributions under the vertex-conformal ansatz. The 3D hinge measure is the conformal edge length $\sqrt{q_e}\exp((\xi_u+\xi_v)/2)$. The line potential is the straight path $t\mapsto t\eta$ through the zero (flat) potential in direction $\eta$. A vertex potential assigns a real number to each vertex of the triangulation.
Upstream, local dihedral directional-derivative packages and conformal Schläfli cancellation identities supply the raw angle derivatives that constructors assemble into this global deficit package.
proof idea
Pure structure definition: three fields with no proof body. The first field is the candidate directional derivative map. The second is the HasDerivAt certificate that this map is the derivative at $t=0$ of deficit angle along the line potential. The third is the global weighted cancellation identity (hinge measures at zero potential times deficit derivatives sum to zero). Downstream constructors such as deficitPackage_of_localAngles and deficitPackage_of_conformalSchlaefliCancellation populate the fields from local dihedral data.
why it matters
This package is the named analytic hypothesis for the directional first-variation formula of the nonlinear Regge action: directionalFirstVariationFormula_of_deficitPackage builds the full first-variation identity directly from it. Constructors deficitPackage_of_localAngles and deficitPackage_of_conformalSchlaefliCancellation show how local angle derivatives plus conformal Schläfli cancellation produce an instance.
It is threaded into cubic Taylor input bundles and into nonlinearRegge_localCorrespondence and strongest-true J-cost replacement theorems, which compare the discrete Regge Hessian to continuum curvature. In the Recognition geometry stack this sits under the D=3 forcing (T8) and the eight-tick triangulation setting: first-variation vanishing at the flat conformal potential is the discrete stationarity step before mass-ladder and curvature-bridge arguments. The module doc states the open expansion work: closed-form local Schläfli identities still need to be fully unwound into these derivative fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.