ReggeActionFirstVariationInput
plain-language theorem explainer
Packages the single analytic hypothesis needed for first-variation vanishing of the nonlinear Regge action on a flat 3D triangulation: the Fréchet derivative of the action at the zero (flat) potential is zero. Anyone proving criticality from directional derivatives, Schläfli cancellation, or incidence bookkeeping cites this structure as the common interface. It is a one-field structure, not a proved theorem.
Claim. For an incidence-consistent 3D Regge triangulation $K$ that admits a flat analytic configuration, a first-variation input is a witness that the Fréchet derivative of the nonlinear Regge action at the zero potential vanishes: $D(\mathrm{Regge\,action})_0 = 0$.
background
The module targets vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric route is Schläfli cancellation plus zero deficit; until the closed-form local identities are fully expanded into a derivative calculation, the module records a named input for that criticality fact.
A Triangulation3D is a finite abstract 3D Regge complex (vertices, edges, tets) with nondegenerate squared-edge data on each tetrahedron. Incidence consistency supplies global squared edge lengths, slot-to-endpoint agreement, and the local closed-form Schläfli data needed for a global identity. A flat configuration adds the arccos endpoint conditions, zero deficit on hinges, and the smoothness needed for Taylor theory.
Criticality at zero is the proposition that the Fréchet derivative of the Regge action at the zero potential is the zero continuous linear map. The structure below simply names that proposition as a field, parameterized by the triangulation, incidence proof, and flatness package.
proof idea
No proof body: this is a structure definition with a single field. The field type is the proposition that the Fréchet derivative of the Regge action at the zero potential vanishes. Downstream constructors inhabit the structure by supplying that field from directional criticality, a first-variation formula, conformal Schläfli cancellation, or incidence/edge-slot bookkeeping. The intended analytic path (per the doc-comment) is: differentiate hinge-length and local dihedral factors, kill the hinge term by zero deficit, then cancel the dihedral term by the global Schläfli identity.
why it matters
This is the shared interface for the module's target: first variation of the nonlinear Regge action vanishes at the flat conformal potential. Many constructors feed it (of_directional, of_firstVariationFormula, of_conformalSchlaefliCancellation, incidence and edge-slot bookkeeping variants), and the main consumer is the theorem that the first variation is zero once such an input is given.
In the Recognition geometry stack this sits under discrete gravity / Regge calculus in three spatial dimensions (T8 forces $D=3$), where flatness and Schläfli identities replace continuum Einstein-Hilbert stationarity. The structure does not close the derivative calculation itself; it freezes the analytic claim so lower-level Schläfli and smoothness work can discharge it without rewriting callers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.