ActionDerivativeFirstOrderTangencyTarget
plain-language theorem explainer
Sharp first-order tangency target for the nonlinear Regge action: along every conformal line through the flat potential, the first derivative of the action is first-order tangent at zero to the ray of the canonical incidence Hessian quadratic. Cited by anyone discharging the nonlinear directional Hessian or building second-variation input packs. Prop-valued definition whose body is a single HasDerivAt condition on the residual; no proof is given here.
Claim. For an incidence-consistent finite 3D triangulation $K$ and every vertex conformal potential $\xi$, the residual map $t\mapsto \partial_t\mathrm{Action}_K(\xi;t)-t\,Q_{H_K}(\xi)$ has derivative $0$ at $t=0$. Here $\mathrm{Action}_K(\xi;t)$ is the nonlinear Regge action along the conformal line through the flat potential in direction $\xi$, $H_K$ is the canonical incidence dual-weight Hessian, and $Q_{H_K}$ is its quadratic form.
background
The module isolates the remaining hard step for the full nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input pack follows at once.
Vertex conformal potentials are maps from the finite vertex set to $\mathbb{R}$. The action along a line is the nonlinear Regge action restricted to the one-parameter conformal family through the flat configuration in direction $\xi$. The canonical Regge Hessian is the graph Laplacian built from incidence dual weights; its quadratic form is $\sum_{i,j}H_{ij}\xi_i\xi_j$.
A stronger sibling target demands that the first derivative of the action equal $t\cdot Q$ identically in a neighborhood of zero (after product rule, Cayley-Menger/arccos, hinge, and Schl"afli cancellations). The present target only asks for first-order contact at the origin, so cubic and higher Regge terms are permitted.
proof idea
Definition, not a theorem. The body is the proposition that for every vertex potential $\xi$, the residual
$$t\mapsto \partial_t(\mathrm{action\ along\ line})(t)-t\cdot Q_{H_K}(\xi)$$
has derivative $0$ at $t=0$ (Mathlib HasDerivAt with value $0$ at point $0$). No lemmas are applied and no obligations are discharged; the declaration only names this interface Prop.
why it matters
This is the sharp interface hypothesis that unlocks the nonlinear directional Hessian theorem: given the tangency target, that theorem follows by unfolding the second-derivative predicate. The same hypothesis feeds the constructions of second-variation and remainder-second-variation input packs under a flat configuration, and the vanishing of the canonical remainder second variation.
The module states that the target is not a new physical assumption but the exact endpoint of the second chain-rule calculation on the nonlinear Regge action. Relative to the stronger neighborhood-linearization target, this version tolerates cubic and higher terms, matching the genuine nonlinear action.
In the Recognition geometry layer it closes the discrete second-variation step that identifies the conformal Hessian with the incidence dual Laplacian on 3D triangulations (spatial dimension $D=3$ from the forcing chain).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.