half_hessianQuadratic_hasFDerivAt_zero
plain-language theorem explainer
At the zero vertex potential on a 3D triangulation, the map sending a potential to half the Hessian quadratic form has Fréchet derivative zero. Anyone assembling the Regge Taylor split (action = constant + quadratic + remainder) cites this to kill the linear term of the quadratic piece. The proof is a one-line scaling of the unscaled Hessian-quadratic derivative lemma.
Claim. For any 3D triangulation $K$ and any real bilinear form $H$ on the vertices, the map $\xi \mapsto \tfrac12\,Q_H(\xi)$ from vertex potentials to $\mathbb{R}$ is Fréchet differentiable at the zero potential, with derivative the zero continuous linear map $V\to\mathbb{R}$.
background
This module targets the vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric engine is Schläfli cancellation plus zero deficit; the analytic work packages that statement as named first-variation inputs until the closed-form local Schläfli identities are fully expanded.
A vertex potential on $K$ is a real assignment to the vertices. The zero potential is the flat base point. The Hessian quadratic $Q_H(\xi)$ is the quadratic form built from a fixed bilinear kernel $H$ on vertex pairs; the Regge Taylor split subtracts a constant and this quadratic piece from the action, leaving a nonlinear remainder.
The unscaled companion result already shows that $\xi\mapsto Q_H(\xi)$ has Fréchet derivative zero at the zero potential. The half-scaled version is the exact coefficient appearing in the Taylor remainder bookkeeping.
proof idea
One-line wrapper. Apply the unscaled lemma hessianQuadratic_hasFDerivAt_zero to obtain HasFDerivAt for $\xi\mapsto Q_H(\xi)$ at the zero potential with derivative zero, then scale by the constant $1/2$ via HasFDerivAt.const_mul. simpa cleans the resulting scalar arithmetic. No triangulation geometry is reopened.
why it matters
Feeds directly into reggeActionRemainderFirstVariationInput_of_firstVariation, which builds the remainder first-variation input from the full Regge first-variation input: "the subtracted constant has zero derivative and the subtracted quadratic Hessian term has zero derivative at the flat point."
Without this half-scaled vanishing, the Taylor split would leave a spurious linear term in the quadratic piece, blocking the claim that the nonlinear remainder alone carries the first variation. That claim is the analytic half of the module target: first variation of the full nonlinear Regge action vanishes at the flat conformal potential (Schläfli cancellation plus zero deficit).
In the broader Recognition geometry stack this sits under the discrete curvature / Regge side of the forcing chain's spatial geometry (T8, $D=3$), packaging the analytic input needed before the closed-form local Schläfli identities discharge the full derivative calculation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.