reggeActionFirstVariationInput_of_firstVariationFormula
plain-language theorem explainer
Packages the directional first-variation formula plus flat zero-deficit into the named first-variation input for the nonlinear Regge action on a 3D triangulation. Anyone proving criticality at the flat conformal potential cites this bridge. The body is a one-line application of the formula-plus-zero-deficit criticality lemma using the flat configuration's deficit field.
Claim. Given a 3D triangulation $K$ with consistent incidence, a flat analytic configuration at the zero potential, and an explicit directional first-variation formula for the nonlinear Regge action at that base point, one obtains the named first-variation input: the Regge action is critical at the zero 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; until the full derivative expansion is written out, the module records the exact analytic statement and the named inputs that stand in for that work.
A flat configuration supplies three facts: arccos endpoint freeness for local dihedral cosines, global zero deficit at the flat base point, and the smoothness needed for Taylor theory. The first-variation formula structure asserts that the Fréchet derivative of the Regge action at the zero potential, applied to any vertex potential $\eta$, equals the sum over edges of (hinge-measure directional derivative of $\eta$) times (deficit angle at zero). The named input structure simply packages criticality at zero under a flat configuration.
Upstream, criticality follows from the directional formula once global zero deficit is known: each summand vanishes, so the derivative is zero in every direction.
proof idea
One-line wrapper. Feed the triangulation, incidence hypothesis, the flat configuration's flat_deficit_zero field (as global zero deficit at flat), and the assumed first-variation formula into reggeActionCriticalAtZero_of_firstVariationFormula_of_zeroDeficit. That theorem reduces to the directional criticality lemma, which kills every term in the edge sum because deficits vanish. The resulting criticality proof fills the single field of ReggeActionFirstVariationInput.
why it matters
Closes the packaging step between the explicit directional first-variation formula and the named input that downstream constructions expect. The immediate consumer is reggeActionFirstVariationInput_of_localAngles, which builds the same input from a local dihedral directional-derivative package plus conformal Schläfli cancellation rather than from a pre-packaged formula.
In the module's program, this sits on the path to the target theorem: first variation of the nonlinear Regge action vanishes at the flat conformal potential. That is the discrete variational statement underlying flat criticality in the Recognition geometry stack (Regge action on 3D triangulations, Schläfli identities, conformal potentials). It does not itself finish the hard differentiation of hinge and dihedral terms; it only records that once the formula and zero deficit are in hand, the named input is filled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.