reggeActionRemainderFirstVariationInput_of_firstVariation
plain-language theorem explainer
Whenever the full nonlinear Regge action has vanishing first variation at the flat zero potential, so does the nonlinear remainder after subtracting the constant value and the half-Hessian quadratic. Gravity and discrete-geometry workers cite this to convert a full first-variation package into the remainder jet required by periodic edge-stencil correspondence. The construction is pure calculus: constant and quadratic terms each have zero Fréchet derivative at zero, so they drop out of the difference.
Claim. Let $K$ be an incidence-consistent 3D triangulation that is flat at the zero vertex potential, and let $H$ be a real matrix on vertex pairs. If the Regge action $S$ satisfies $DS(0)=0$, then the nonlinear remainder $R(\xi)=S(\xi)-S(0)-\tfrac12 Q_H(\xi)$ also satisfies $DR(0)=0$, where $Q_H$ is the Hessian quadratic form associated to $H$.
background
This module records the analytic first-variation package for the nonlinear 3D Regge action under a vertex-conformal ansatz. The concrete action is a sum over edges of hinge measure times deficit angle. The target geometric fact is that the first variation vanishes at the flat conformal potential, by Schläfli cancellation plus zero deficit; until that derivative is expanded in closed form, the module packages the claim as a named input structure.
ReggeActionFirstVariationInput asserts that the full action is critical at the zero potential. ReggeActionRemainderFirstVariationInput asserts the same for the Taylor remainder after subtracting the constant value $S(0)$ and the half-Hessian quadratic $\tfrac12 Q_H$. The remainder input is kept separate because its proof needs the quadratic form's derivative in the same finite-dimensional calculus universe as the action.
Upstream, half_hessianQuadratic_hasFDerivAt_zero already shows that the scaled Hessian term has zero Fréchet derivative at zero. Flatness supplies continuous differentiability of the action at the zero potential.
proof idea
Build the remainder first-variation structure by proving remainder_firstVariation_zero.
- From flatness, the action is differentiable at the zero potential; rewrite its Fréchet derivative using the hypothesis that the first variation vanishes, obtaining
HasFDerivAt S 0at zero. - The constant map $\xi\mapsto S(0)$ has Fréchet derivative zero (
hasFDerivAt_const). - Apply
half_hessianQuadratic_hasFDerivAt_zeroso $\xi\mapsto\tfrac12 Q_H(\xi)$ also has derivative zero at zero. - Subtract:
HasFDerivAtis linear, so $S-S(0)-\tfrac12 Q_H$ has derivative zero. Convert to thefderivform required by the structure field.
why it matters
The remainder jet is the analytic input that gravity instances actually consume. Downstream, canonicalPeriodicEdgeStencilLocalCorrespondence_of_canonicalFlat_first_and_directionalHessian takes a ReggeActionRemainderFirstVariationInput together with a nonlinear directional Hessian theorem and produces periodic edge-stencil local correspondence on the canonical Freudenthal torus. Its sibling ..._of_canonicalFlat_firstVariationInput_and_directionalHessian accepts the fuller first-variation package and explicitly routes through this constructor, so callers need not re-derive the constant/quadratic cancellation.
In the Recognition geometry stack this sits under the discrete gravity path: flat conformal configurations on 3D triangulations, first variation of the Regge action, then local stencil correspondence. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure calculus packaging that keeps the remainder hypothesis dischargeable once the full Schläfli first-variation proof lands.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.