deficitPackage_of_localAngles
plain-language theorem explainer
Packages local dihedral directional derivatives plus a global hinge-weighted cancellation hypothesis into the deficit-angle derivative package required by conformal Regge first variation. Anyone assembling the first-variation vanishing argument at the flat conformal potential cites this constructor. It is a pure structure assembly: deficit derivatives come from the local-angle sum, HasDerivAt is the existing local-to-global lemma, and cancellation is the supplied hypothesis.
Claim. Given a 3D triangulation $K$ with consistent incidence, a package of directional derivatives of the local dihedral angles under the conformal line potential, and the hypothesis that for every vertex potential $\eta$ the sum over edges of (hinge measure at the zero potential) times (deficit directional derivative from those local angles) vanishes, one obtains a deficit-angle directional-derivative package whose derivative field is that local-angle construction, whose $\mathrm{HasDerivAt}$ facts are the corresponding local-to-global facts, and whose Schläfli cancellation field is exactly the given hypothesis.
background
The module targets vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric engine is Schläfli cancellation together with zero deficit; this file records the analytic packaging until closed-form local Schläfli identities are fully expanded.
A LocalDihedralDirectionalDerivativePackage supplies, for each tetrahedron face index, a directional derivative of the conformal dihedral angle along the line potential $t \mapsto$ linePotential$(\eta,t)$, with a matching HasDerivAt certificate at $t=0$. Deficit angles on edges are assembled from those local dihedrals; the companion lemma deficitAngle_hasDerivAt_from_localAngles lifts the local certificates to edge deficits.
The hinge measure under the conformal ansatz is the edge length: $\sqrt{\text{global squared edge}}\cdot\exp((\xi_u+\xi_v)/2)$. The global Schläfli contribution in a conformal direction is the edge sum of hinge measure (at the zero potential) times the deficit directional derivative. The target structure DeficitAngleDirectionalDerivativePackage packages exactly those three pieces: a deficit derivative field, its HasDerivAt facts, and the cancellation identity.
proof idea
Definitional structure constructor, not a proof. The deficit derivative field is set to deficitDirectionalDerivFromLocalAngles K A. The HasDerivAt field is filled by the already-proved lemma deficitAngle_hasDerivAt_from_localAngles K A. The Schläfli cancellation field is the input hypothesis hCancel verbatim. No new analytic work occurs here.
why it matters
This is the bridge from local dihedral calculus to the global deficit package that the conformal first-variation argument consumes. Downstream, deficitPackage_of_conformalSchlaefliCancellation is a one-line specialization: it feeds a named ConformalSchlaefliCancellation hypothesis into this constructor. The module goal is vanishing of the first variation of the nonlinear Regge action at the flat conformal potential; that vanishing is Schläfli cancellation plus zero deficit. By isolating the cancellation hypothesis as an explicit field, the definition keeps the analytic gap (proving cancellation from local Schläfli identities) cleanly separated from the packaging used by later variation lemmas. In the broader Recognition geometry stack this sits under the discrete curvature / Regge side that eventually interfaces with the forced $D=3$ and eight-tick structure, but the declaration itself is pure 3D triangulation analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.