reggeActionFirstVariationInput_of_localAngles
plain-language theorem explainer
Builds the named first-variation input for the nonlinear Regge action from a local dihedral directional-derivative package plus conformal Schläfli cancellation, on a flat incidence-consistent 3D triangulation. Cited by anyone assembling criticality of the Regge action at the zero conformal potential. Proof is a pure four-step composition of intermediate package converters.
Claim. Let $K$ be an incidence-consistent 3D triangulation that is flat. Given a package $A$ of local dihedral-angle directional derivatives under the conformal ansatz, and given that the conformal Schläfli cancellation identity holds for $A$, produce a first-variation input package witnessing that the Regge action is critical at the zero vertex potential.
background
This 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; the analytic work is packaged until the closed-form local Schläfli identities are fully expanded into derivatives.
A local dihedral directional-derivative package supplies, for each vertex potential $\eta$, tetrahedron $\tau$, and face-pair index $f$, the real number that is the derivative at $t=0$ of the dihedral angle of $\tau$ along the conformal line potential generated by $\eta$. Conformal Schläfli cancellation then asserts that, for every such $\eta$, the edge-sum of hinge measure (evaluated at the zero potential) times the deficit directional derivative built from those local angles vanishes.
The output type is a named first-variation input: a structure whose sole field is the statement that the Regge action is critical at zero on the given flat configuration. Upstream converters turn cancellation into a deficit-angle package, then into a directional first-variation formula, then into a full first-variation formula.
proof idea
One-line composition of four already-defined converters. First apply the converter that turns the local-angle package plus conformal Schläfli cancellation into a deficit-angle directional-derivative package. Feed that into the theorem that extracts a directional first-variation formula from any deficit package. Lift the directional formula to a full first-variation formula. Finally wrap that formula as a named first-variation input via the corresponding constructor. No new analytic work occurs at this layer.
why it matters
Sits in the middle of the assembly line that proves the Regge action is critical at the flat conformal potential. Two immediate parents reuse it: one specializes the local-angle package to the flat-configuration package, and one routes through incidence bookkeeping and the length-chain rule. The module doc states the target theorem is vanishing of the first variation; this definition is the named input that theorem consumes once Schläfli cancellation and local angle derivatives are in hand. In the broader Recognition geometry stack it records the exact analytic interface between discrete Schläfli identities on a 3D triangulation and the continuum first-variation statement, without yet expanding the arccos/cofactor derivatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.