ReggeActionRemainderFirstVariationInput
plain-language theorem explainer
Packages the hypothesis that the Fréchet derivative of the nonlinear Regge-action remainder vanishes at the zero conformal potential. Cubic Taylor and line-jet closures cite it as a named first-variation input beside flatness and second-variation data. As a structure it is pure interface: one field asserting that identity for fixed triangulation, incidence consistency, and Hessian matrix.
Claim. For a 3D triangulation $K$ with consistent incidence and a real bilinear form $H$ on vertex pairs, the structure asserts that the Fréchet derivative of the nonlinear Regge remainder $R_K(\xi)=S_K(\xi)-S_K(0)-\tfrac12 Q_H(\xi)$ vanishes at the zero vertex potential: $DR_K(0)=0$.
background
This 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 Schläfli identities are expanded into a full derivative calculation, the analytic statement is recorded via named inputs.
The nonlinear remainder subtracts the action value at zero and a candidate quadratic Hessian term from the full Regge action: $R_K(\xi)=S_K(\xi)-S_K(0)-\tfrac12 Q_H(\xi)$. The zero conformal potential is the zero section on vertices. The Hessian matrix $H$ is the candidate second-derivative form used to peel off the quadratic piece.
Recording the first-variation identity separately keeps the finite-dimensional quadratic form's derivative at zero in the same analytic universe as the full action, so later jet and Taylor arguments can treat it as a clean hypothesis rather than an inlined calculation.
proof idea
No proof body: this is a structure definition with a single field. The field is the proposition that the Fréchet derivative of reggeActionRemainder at zeroPotential equals the zero continuous linear map. Instantiation is by supplying a proof of that identity for the chosen triangulation, incidence hypothesis, and Hessian matrix.
why it matters
This is the first-variation jet input in the cubic Taylor cascade for the canonical remainder. Downstream, CanonicalRemainderCubicTaylorFromJetInputsTarget isolates the remaining finite-dimensional Taylor theorem as: given this input plus the second-variation input, obtain the local $O(|\xi|^3)$ bound. Closures such as canonicalRemainderLine_hasDerivAt_zero_of_remainderFirstVar, canonicalRemainderLineQuadraticTaylorZero_of_jetInputs, and canonicalRemainderLineTaylorData_of_flat_and_remainderJets thread it into line-restricted derivatives and degree-2 Taylor data at zero.
CanonicalRemainderAnalyticClosureCert packages the full cascade from flat configuration plus these jet inputs. In the Recognition geometry stack this sits under the analytic control of the nonlinear Regge action near flat conformal potentials (Schläfli plus zero deficit), feeding higher-order remainder estimates rather than the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.