hessianQuadratic_hasFDerivAt_zero
plain-language theorem explainer
The quadratic Hessian form on vertex potentials of a 3D triangulation has vanishing Fréchet derivative at the zero potential. Anyone assembling the Taylor split of the nonlinear Regge action cites this to kill the linear term in the quadratic piece. The proof is a double Finset-sum reduction to the single-term vanishing lemma.
Claim. For any 3D triangulation $K$ and any real matrix $H$ indexed by pairs of vertices, the map $\xi \mapsto Q_H(\xi)$ sending a vertex potential to the associated quadratic Hessian form is Fréchet differentiable at the zero potential, with derivative the zero continuous linear map $0 : V(K) \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 side records exact derivative statements needed until the closed-form local Schläfli identities are fully expanded.
A vertex potential on $K$ is a real assignment to the vertices of the triangulation. The zero potential is the identically zero assignment. The quadratic Hessian form $Q_H$ is built as a double finite sum over vertex pairs of bilinear terms weighted by the matrix $H$; it is the quadratic piece appearing in the Taylor split of the Regge action about flat conformal data.
Upstream, each individual summand already has zero Fréchet derivative at zero (hessianQuadratic_term_hasFDerivAt_zero), and finite sums of maps with zero derivative at a point again have zero derivative there (hasFDerivAt_finset_sum_zero). Those two facts are the only analytic inputs.
proof idea
Unfold the definitions of the quadratic Hessian and of the zero potential, exposing a double Finset.sum. Apply the finite-sum zero-derivative lemma once for the outer sum and once for the inner sum. On each summand, invoke the single-term lemma hessianQuadratic_term_hasFDerivAt_zero (with a simpa to align the zero-potential unfolding). No further calculus is required: the result is pure sum-stability of HasFDerivAt at zero.
why it matters
In the Regge Taylor split, the action near the flat conformal potential decomposes into quadratic Hessian, higher-order remainder, and geometric deficit terms. Vanishing of the first variation of the quadratic piece is mandatory so that the linear response is carried only by the deficit/Schläfli sector, which cancels at flatness.
The immediate parent is half_hessianQuadratic_hasFDerivAt_zero, which scales by $1/2$ for the conventional Taylor coefficient. Together they clear the quadratic channel in the module's target: first variation of the full nonlinear Regge action at the flat conformal potential. That target sits in the geometry layer supporting continuum limits and curvature identification in Recognition Science, downstream of the Schläfli tetrahedron and 3D triangulation infrastructure (imports SchlaefliTetrahedronProof, SchlaefliTriangulation3D).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.