ActionDerivativeLinearizationNearZeroTarget
plain-language theorem explainer
Exact first-derivative linearization target for the nonlinear Regge action: along every conformal line through a vertex potential, the action derivative equals t times the canonical Hessian quadratic form in a neighborhood of the flat point t=0. Anyone closing the second-variation chain cites this Prop. It is a definition of the residual geometric identity after product rule, Cayley-Menger, hinge, and Schläfli expansions, not a proved theorem.
Claim. For an incidence-consistent 3-dimensional triangulation $K$ and every vertex potential $\xi$, the map $t \mapsto \frac{d}{dt}S_K(\xi_t)$ is eventually equal, in a neighborhood of $t=0$, to $t \mapsto t\,Q_{H(K)}(\xi)$, where $S_K$ is the Regge action along the conformal line through $\xi$ and $Q_{H(K)}$ is the quadratic form of the canonical incidence Hessian of $K$.
background
The module isolates the hard endpoint of the nonlinear Regge second-variation calculation: at a flat vertex potential the second directional derivative of the full Regge action must recover the canonical incidence Hessian. The action is evaluated along conformal lines $t \mapsto \xi_t$ in the space of vertex potentials on an incidence-consistent triangulation $K$.
After expanding the local geometric product rule, Cayley-Menger and arccos edge derivatives, hinge derivatives, and Schläfli cancellation near the flat point, a residual first-derivative identity remains. That identity is stronger than a bare derivative-at-zero claim: the derivative of the action along the line must match the linear function $t \mapsto t,Q_H(\xi)$ throughout a neighborhood of zero, not merely at the origin.
The right-hand side uses the canonical Regge Hessian of $K$ and its associated quadratic form on vertex potentials. Downstream material also splits the action into a canonical quadratic piece plus a remainder along each line.
proof idea
Definitional Prop, not a proof. The body is a single universal quantifier over vertex potentials $\xi$, asserting filter equality $=^{\mathrm{f}}[$nhds $0]$ between the real function $t \mapsto \mathrm{deriv}(\mathrm{actionAlongLine},K,hK,\xi),t$ and the linear map $t \mapsto t\cdot\mathrm{hessianQuadratic}(\mathrm{canonicalReggeHessian},K,hK),\xi$. No tactics or lemmas are applied; the declaration only names the residual geometric target.
why it matters
This target is the exact interface the module was built to isolate. Once inhabited, it immediately yields the nonlinear directional Hessian theorem (nonlinearDirectionalHessian_of_actionDerivativeLinearizationNearZero), first-order tangency (actionDerivativeFirstOrderTangency_of_linearizationNearZero), vanishing of the canonical remainder second variation under flatness, and both ReggeActionSecondVariationInput and ReggeActionRemainderSecondVariationInput constructors under a flat configuration.
In the Recognition geometry stack this closes the second chain-rule calculation that turns discrete Regge calculus into the continuum Hessian used for curvature and mass-ladder geometry. The module doc states the theorem is not a new assumption but the endpoint of that expansion; supplying a proof of this Prop discharges the remaining hard step and lets the existing second-variation infrastructure fire without further hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.