reggeAction_firstVariation_zero
plain-language theorem explainer
At a flat conformal configuration on an incidence-consistent 3D triangulation, the Fréchet derivative of the nonlinear Regge action vanishes at the zero vertex potential, once the named analytic first-variation input is supplied. Discrete-gravity and Regge-calculus workers cite this as the critical-point statement for the vertex-conformal ansatz. The proof is a one-line unpack of that input's criticality field.
Claim. Let $K$ be an incidence-consistent 3D triangulation admitting a flat configuration, and assume the named analytic first-variation input at that flat point. Then the Fréchet derivative of the conformal Regge action at the zero vertex potential is the zero map: $D(\mathrm{Regge}_K)(0)=0$.
background
The module fixes the analytic first-variation problem for the full nonlinear Regge action under the vertex-conformal ansatz. Concretely, the action on a potential $\xi$ is the edge sum of conformal hinge measure times deficit angle. A flat configuration means every deficit vanishes at the zero potential, so the base geometry is Euclidean.
The named first-variation input is a structure whose single field asserts criticality of the action at zero. Its intended lower-level content (per its doc) 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. Upstream concrete action, flat-configuration, and Schläfli tetrahedron/triangulation results supply that geometric engine; this declaration only packages the resulting criticality statement.
proof idea
One-line term proof. The goal is definitionally the field firstVariation_zero carried by the hypothesis structure that packages analytic criticality at the zero potential. No differentiation, no Schläfli identity, and no summation is performed here; the theorem is the public re-export of that packaged fact.
why it matters
Phase-C first-variation theorem for the nonlinear Regge action in the Recognition geometry stack. It records that flat conformal potentials are critical points of the discrete Einstein-Hilbert functional, the discrete analogue of vacuum criticality for the Einstein equations. The module states the geometric engine explicitly: Schläfli cancellation plus zero deficit. No downstream consumers are wired yet, so the declaration presently closes the first-variation interface rather than feeding a named parent theorem. It sits on the continuum-bridge path that identifies simplicial ledger action with hinge-deficit curvature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.