actionDerivativeFirstOrderTangency_of_quadraticTangency
plain-language theorem explainer
First-order tangency of the full Regge action derivative to the canonical Hessian line follows from tangency to the derivative of the canonical quadratic along each conformal line. Anyone wiring the geometric quadratic form into the nonlinear directional Hessian cites this bridge. The proof is a convert-and-rewrite that substitutes the explicit derivative of the canonical quadratic along a line.
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) - \partial_t Q^{\mathrm{can}}_K(t\xi)$ has derivative zero at $t=0$. Then for every $\xi$, the map $t \mapsto \partial_t S_K(t\xi) - t\, H^{\mathrm{can}}_K(\xi,\xi)$ also has derivative zero at $t=0$.
background
This 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. The endpoint is not a new assumption; once the chain-rule calculation is supplied, ReggeActionSecondVariationInput follows at once.
Two equivalent first-order targets appear. The sharp target asks that, along every conformal line $t\mapsto t\xi$, the derivative of the action be first-order tangent at $t=0$ to the linear map $t\mapsto t,H^{\mathrm{can}}(\xi,\xi)$, allowing cubic and higher Regge terms. The geometric twin phrases the same condition against the actual one-variable derivative of the canonical quadratic along that line, rather than the simplified scalar formula.
The bridge between them is the identity $\partial_t Q^{\mathrm{can}}(t\xi)=t,H^{\mathrm{can}}(\xi,\xi)$, already proved as the derivative of the canonical quadratic along a line. Incidence consistency of the 3D triangulation is the standing geometric hypothesis throughout.
proof idea
Fix a vertex potential $\xi$ and apply the geometric tangency hypothesis to it. The two target predicates differ only in the comparison term inside the HasDerivAt difference: one subtracts $\partial_t Q^{\mathrm{can}}$, the other subtracts $t,H^{\mathrm{can}}(\xi,\xi)$. A convert ... using 1 followed by pointwise extensionality reduces the goals to equality of those comparison terms. Rewrite with deriv_canonicalQuadraticAlongLine, which states exactly $\partial_t Q^{\mathrm{can}}(t\xi)=t,H^{\mathrm{can}}(\xi,\xi)$, and the goals close.
why it matters
This is the glue lemma that lets the rest of the nonlinear Hessian stack accept the geometric (quadratic-line) form of first-order tangency. Downstream, nonlinearDirectionalHessian_of_actionDerivativeTangencyToQuadratic applies it and then the first-order-tangency route to obtain the full nonlinear directional Hessian theorem. The same bridge feeds the constructors that build ReggeActionSecondVariationInput and the remainder second-variation input from a flat configuration plus quadratic tangency.
In the Recognition geometry layer this closes a packaging gap rather than a physical gap: the hard calculation remains the chain-rule verification that the action derivative really is tangent to the canonical quadratic. Once that geometric target is proved, this lemma and its parents deliver equality of the second directional derivative at the flat point with the canonical incidence Hessian, the module's stated endpoint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.