ActionDerivativeTangencyToQuadraticTarget
plain-language theorem explainer
Packages the geometric tangency target: along every conformal line through the flat potential, the difference between the first derivatives of the nonlinear Regge action and of the canonical quadratic has derivative zero at the origin. Cited by anyone discharging the nonlinear directional Hessian or second-variation input. Pure Prop definition wrapping a HasDerivAt statement; no proof content.
Claim. For an incidence-consistent finite 3D triangulation $K$ and every vertex conformal potential $\xi$, the real map $t \mapsto \partial_t\,S_K(\xi_t) - \partial_t\,Q_K(\xi_t)$ is differentiable at $t=0$ with derivative $0$, where $\xi_t$ is the conformal line through the flat potential in direction $\xi$, $S_K$ is the nonlinear Regge action, and $Q_K$ is the canonical quadratic of the incidence Hessian along that line.
background
The module isolates the remaining hard step for the full nonlinear Regge Hessian: the second directional derivative of the Regge action at the flat potential must equal the canonical incidence Hessian. Once that calculation is in hand, ReggeActionSecondVariationInput follows at once.
A finite 3D triangulation $K$ carries abstract incidence data and nondegenerate squared-edge lengths on each tetrahedron. Vertex conformal potentials are maps from vertices to $\mathbb{R}$. The nonlinear action restricted to the conformal line through the flat potential in direction $\xi$ is actionAlongLine; the matching canonical quadratic along that line is half the Hessian quadratic form of the incidence Hessian evaluated on the line potential.
This target is the geometric phrasing of tangency against the actual derivative of that canonical quadratic line, rather than a simplified scalar formula.
proof idea
Definitional packaging only: the body is the universal quantification over vertex potentials $\xi$ of HasDerivAt for the difference of first derivatives of actionAlongLine and canonicalQuadraticAlongLine, with value and point both zero. No tactics, no lemmas applied.
why it matters
This is the central geometric interface in the nonlinear Regge Hessian proof chain. Downstream, actionDerivativeFirstOrderTangency_of_quadraticTangency converts it into first-order tangency, and nonlinearDirectionalHessian_of_actionDerivativeTangencyToQuadratic lifts that to the full nonlinear directional Hessian theorem (second directional derivative equals the canonical incidence Hessian at the flat potential).
Several discharge routes feed into it: product-rule tangency near zero, flat product-rule derivative of the canonical Hessian, and combinations of weighted-deficit stationarity (or eventual vanishing) with mixed-hinge edge stencils. Those then produce the second-variation and remainder second-variation inputs under flatness. In the Recognition geometry stack this closes the second chain-rule calculation that makes the discrete Regge Hessian match its continuum quadratic model in $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.