ReggeActionDirectionalFirstVariationFormula
plain-language theorem explainer
Packages the directional first-variation identity for the 3D conformal Regge action: along every line tη through the flat potential, d/dt of the action at t=0 equals the sum over edges of (hinge-length directional derivative times flat deficit). Cited by anyone reducing first-variation vanishing to one-variable product-rule calculus. It is a structure recording that claim, not a proved theorem.
Claim. For an incidence-consistent 3D triangulation $K$, the structure asserts: for every vertex potential $\eta$, the real map $t \mapsto S_{\mathrm{Regge}}(K, t\eta)$ has derivative at $t=0$ equal to $\sum_e \ell'_e(\eta)\,\delta_e(0)$, where $\ell'_e(\eta)$ is the directional derivative of conformal hinge length at the flat potential and $\delta_e(0)$ is the Regge deficit on edge $e$ at the zero potential.
background
The module targets vanishing of the first variation of the full nonlinear 3D Regge action at the flat conformal potential. The geometric engine is Schläfli cancellation plus zero deficit; analytically one first needs a clean one-variable derivative identity along lines through the origin in potential space.
Under the vertex-conformal ansatz the action is $S=\sum_e \ell_e(\xi),\delta_e(\xi)$, with hinge measure $\ell_e$ the conformal edge length and deficit $\delta_e=2\pi-\sum_\tau$ local dihedral contributions. The line potential is $t\mapsto t\eta$ through the flat (zero) potential. The hinge directional derivative at flat is $\sqrt{q_e},(\eta_u+\eta_v)/2$ on the endpoints of edge $e$.
This structure isolates the product-rule form of $dS/dt|_{t=0}$ before assembling the full Fréchet first-variation statement.
proof idea
No proof body: the declaration is a structure whose single field is a proposition. Inhabitants are built downstream by supplying a proof that, for every direction $\eta$, the composite $t\mapsto S(t\eta)$ has the stated HasDerivAt value at $0$. The intended route is one-variable differentiation of the edgewise product $\ell_e(t)\delta_e(t)$, using the closed-form hinge derivative and a deficit-angle directional package; the structure itself only names the target identity.
why it matters
This is the intermediate analytic interface between local Schläfli/deficit derivative packages and the full first-variation formula. Downstream, directionalFirstVariationFormula_of_deficitPackage builds an inhabitant from a deficit-angle directional derivative package, and firstVariationFormula_of_directionalFormula lifts any such inhabitant (plus flatness) to the Fréchet first-variation formula at the flat configuration.
In the Recognition geometry stack this sits under the program that the nonlinear Regge action is stationary at the flat conformal potential, the discrete precursor to continuum Einstein-Hilbert stationarity. It does not itself invoke T0–T8 or the RCL; it is pure Regge calculus scaffolding needed before curvature-balance and continuum limits are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.