hessianQuadratic_term_hasFDerivAt_zero
plain-language theorem explainer
Each bilinear monomial H_{ij} ξ_i ξ_j on vertex potentials of a 3D triangulation is Fréchet differentiable at the zero potential, with derivative the zero map. Anyone assembling the first variation of the quadratic Hessian form of the Regge action cites this termwise fact. The proof is the product rule on coordinate projections: both factors vanish at the origin, so the derivative collapses to zero.
Claim. Let $K$ be a finite 3D triangulation and $H$ a real matrix on its vertices. For any vertices $i,j$, the map $\xi \mapsto H_{ij}\,\xi_i\,\xi_j$ from vertex potentials $\xi$ to $\mathbb{R}$ has Fréchet derivative equal to the zero continuous linear map at the zero potential.
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 is to make the derivative of the action (and of its quadratic Hessian piece) rigorous on a discrete 3D triangulation.
A vertex potential is a real assignment to the finitely many vertices of $K$. The zero potential is the zero assignment. The quadratic Hessian form is assembled from bilinear monomials $H_{ij}\xi_i\xi_j$; the present lemma treats one such monomial. Continuous linear projections extract the $i$-th and $j$-th coordinates, and Mathlib's Fréchet calculus supplies the product rule for their scaled product.
Upstream cost-algebra and constant symbols appear only as ambient imports; the local argument is pure finite-dimensional calculus on $\mathbb{R}^{n_V}$.
proof idea
Define the continuous linear evaluation maps $\mathrm{eval}i$ and $\mathrm{eval}j$ (coordinate projections). Each is its own Fréchet derivative at every point, hence at the zero potential. Scale the first by the constant $H{ij}$ via const_mul. Apply the product rule (HasFDerivAt.mul) to obtain the derivative of $\xi\mapsto H{ij}\xi_i\xi_j$. Convert: at the zero potential both factors vanish, so the product-rule formula $f'g+fg'$ is the zero map. A one-line ext/simp on the zero potential finishes the identification.
why it matters
The sole downstream consumer is hessianQuadratic_hasFDerivAt_zero, which lifts termwise vanishing to the full quadratic Hessian form: the sum of the monomials likewise has zero first derivative at the zero potential. That fact is a named analytic input toward the module's target, the vanishing of the first variation of the nonlinear Regge action at the flat conformal potential.
In the Recognition framework this sits on the geometry side of the forcing chain: spatial dimension $D=3$ (T8) and the discrete triangulation setting in which Schläfli identities cancel deficits. It does not itself invoke the J-cost, RCL, or phi-ladder; it clears a calculus obligation so those geometric identities can be fed into a clean first-variation statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.