reggeActionRemainder_fderiv_zero
plain-language theorem explainer
At the flat conformal potential, the Fréchet derivative of the nonlinear Regge-action remainder vanishes. Anyone assembling the first-variation identity for the full nonlinear Regge action cites this projection. The proof is a one-line field extraction from the named remainder-first-variation input structure.
Claim. Let $K$ be an incidence-consistent 3D triangulation and $H$ a bilinear form on vertex potentials. If the remainder first-variation input holds for $(K,H)$, then the Fréchet derivative of the nonlinear Regge-action remainder at the zero (flat) potential is the zero map: $D R_{K,H}(0) = 0$.
background
The module records the analytic first variation of the nonlinear Regge action on a finite 3D triangulation. The geometric target is vanishing of that first variation at the flat conformal potential, by Schläfli cancellation plus zero deficit.
The remainder is the nonlinear Taylor leftover after subtracting the action at zero and half a candidate Hessian quadratic form: $R(\xi)=S(\xi)-S(0)-\tfrac12 Q_H(\xi)$. The named input structure packages the claim that this remainder has vanishing first derivative at zero. That claim is kept separate because proving it needs the derivative of the finite-dimensional quadratic form in the same analytic universe as the full action.
The evaluation point is the zero vertex potential (flat conformal background).
proof idea
One-line wrapper. The hypothesis is a structure whose single field is exactly the identity $\mathrm{fderiv},\mathbb{R},(R_{K,H})(0)=0$. The proof projects that field.
why it matters
This sits in the first-variation pipeline for the nonlinear Regge action. The module target is vanishing of the first variation of the full nonlinear action at the flat conformal potential; the geometric engine is Schläfli cancellation plus zero deficit. Packaging the remainder derivative as a named input keeps analytic bookkeeping separate until closed-form local Schläfli identities are expanded into full derivative calculations.
No downstream consumers are recorded yet, so the declaration is presently a local interface theorem inside the geometry stack. In the broader Recognition framework it supports the discrete geometric side of the forcing chain toward $D=3$ (T8), by controlling linear response of the Regge action around flat space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.