actionDerivativeFirstOrderTangency_of_linearizationNearZero
plain-language theorem explainer
If the first derivative of the Regge action along every conformal line equals the canonical Hessian quadratic near the flat point, then that derivative is first-order tangent to the Hessian line at zero. Anyone closing the nonlinear Regge Hessian chain cites this bridge. The proof is a short congruence: the linearization forces the difference to be eventually zero, hence derivative zero at the origin.
Claim. Let $K$ be an incidence-consistent 3D triangulation. Suppose that for every vertex potential $\xi$, the map $t \mapsto \partial_t S_K(t\xi)$ is eventually equal, in a neighbourhood of $t=0$, to $t \mapsto t\,Q_K(\xi)$, where $Q_K$ is the quadratic form of the canonical Regge Hessian. Then for every $\xi$, the difference $\partial_t S_K(t\xi) - t\,Q_K(\xi)$ has derivative $0$ at $t=0$.
background
This module isolates the last hard step of the nonlinear Regge Hessian: the second directional derivative of the full Regge action at the flat potential must match the canonical incidence Hessian. The module doc states that once that calculation is supplied, the existing second-variation input follows immediately.
Two target propositions sit between the expanded geometric product rule and the Hessian theorem. The stronger linearization target asserts that, near $t=0$, the first derivative of the action along each conformal line equals exactly the canonical Hessian line $t\mapsto t,Q_K(\xi)$. The weaker first-order tangency target only asks that the difference between those two maps have derivative zero at the origin, allowing cubic and higher Regge remainders.
Here $S_K(t\xi)$ is the Regge action restricted to the conformal line through the flat potential in direction $\xi$, and $Q_K$ is the quadratic form of the canonical Regge Hessian built from the incidence structure of $K$.
proof idea
Fix a vertex potential $\xi$. The constant-zero map $\mathbb{R}\to\mathbb{R}$ has derivative $0$ at $0$ by the standard constant-derivative lemma. The linearization hypothesis supplies an eventually-equal neighbourhood of $0$ on which $\partial_t S_K(t\xi)=t,Q_K(\xi)$, so the difference map is eventually the zero function. Congruence of derivatives under eventual equality then transfers the zero derivative from the constant map to the difference, which is exactly first-order tangency at the origin. The only algebraic step is a ring rewrite after substituting the linearization identity.
why it matters
In the nonlinear Regge Hessian proof interface, this lemma is the one-way implication from the strong linearization target to the sharp first-order tangency target. Sibling declarations then lift either target to the full nonlinear directional Hessian theorem (second directional derivative at the flat point equals the canonical incidence Hessian).
That Hessian identity is the endpoint of the second chain-rule calculation for the Regge action: after local geometric product rule, Cayley–Menger/arccos derivatives, hinge derivatives, and Schläfli cancellation, what remains is precisely this first-derivative control near the flat point. Closing it discharges the hard half of ReggeActionSecondVariationInput and feeds the Recognition geometry layer where discrete curvature is read off incidence data.
No downstream consumers are wired yet in the graph; the immediate consumers are the in-module Hessian corollaries that take tangency (or linearization) as hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.