ReggeActionFirstVariationFormula
plain-language theorem explainer
Packages the directional first-variation identity for the nonlinear 3D Regge action at the flat conformal potential: the Fréchet derivative in direction η equals the edge sum of hinge-length directional derivatives times flat deficits. Cited by anyone proving discrete vacuum Einstein or criticality at zero deficit. Definitional interface (structure field), not a derived theorem; the analytic content is left as a named hypothesis.
Claim. For an incidence-consistent finite 3D triangulation $K$, the first-variation formula asserts: for every vertex conformal potential $\eta$, the Fréchet derivative of the Regge action $S$ at the zero potential satisfies $DS(0)[\eta]=\sum_e \ell'_e(\eta)\,\delta_e(0)$, where $\ell'_e(\eta)$ is the directional derivative of the conformal hinge (edge) length at flat configuration and $\delta_e(0)$ is the Regge deficit angle of edge $e$ under the zero potential.
background
The module targets vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. Geometry is a finite 3D triangulation $K$ with incidence consistency; configurations are vertex conformal potentials $\xi:V\to\mathbb{R}$, with zero potential the flat background.
The concrete Regge action is $S(\xi)=\sum_e \ell_e(\xi),\delta_e(\xi)$, hinge measure $\ell_e$ the conformal edge length and deficit $\delta_e=2\pi-\sum_\tau\theta_{e,\tau}$ the usual angle defect. The directional hinge derivative at flat is explicit: $\ell'_e(\eta)=\sqrt{q_e},(\eta_u+\eta_v)/2$ on the endpoints of $e$.
Upstream, global Schläfli and local dihedral smoothness supply the angle-side cancellation once the product rule is expanded. This structure records the exact analytic identity those calculations must deliver before criticality is deduced from zero deficit.
proof idea
No proof body: the declaration is a structure whose single field is the stated identity. Inhabitants are produced downstream by converting a one-variable (directional) product-rule form into the Fréchet statement at the flat potential, or are assumed as analytic input until the full hinge/dihedral differentiation plus global Schläfli is expanded from closed-form local identities.
why it matters
This is the named analytic gate between the concrete Regge action and discrete vacuum Einstein. Downstream, assuming the formula plus global zero deficit at flat yields directional criticality and full criticality of $S$ at the zero potential; it also assembles the first-variation input bundle used by the gravity layer.
In DiscreteVacuumEinstein the same pairing (deficit vector against conformal edge-length directions) appears as ReggeFirstVariationFormula, the pre-zero-deficit form of the discrete Einstein equation. Within Recognition geometry this sits under the $D=3$ forcing (T8) and the eight-tick discrete skeleton: the Regge critical point at flat is the discrete vacuum Einstein condition on the triangulation.
The hard remaining work flagged by the doc-comment is deriving the formula itself by differentiating hinge and dihedral terms and applying global Schläfli to kill the angle variation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.