ActionDerivativeProductRuleNearZeroTarget
plain-language theorem explainer
Names the product-rule identity needed near the flat configuration: the derivative of the Regge action along any vertex-potential line equals, in a neighborhood of t = 0, the finite sum of hinge-area and deficit contributions. Downstream Hessian arguments cite this Prop as the first-order chain-rule checkpoint. The body is a pure predicate definition, not a proof.
Claim. For an incidence-consistent 3D triangulation $K$, the product-rule target asserts: for every vertex potential $\xi$, the map $t \mapsto \frac{d}{dt}\,S_K(\xi_t)$ agrees, eventually in a neighborhood of $t=0$, with the explicit product-rule derivative built from hinge and deficit factors along that line.
background
This module isolates the hard second-variation calculation for the full nonlinear Regge action: at the flat potential, the second directional derivative must match the canonical incidence Hessian. The module doc frames the endpoint as ordinary chain-rule work, after which the existing second-variation input package follows at once.
The Regge action along a line is the restriction of the discrete action to the affine path $t \mapsto$ flat configuration plus $t\xi$ in the space of vertex potentials on $K$. Its $t$-derivative is an ordinary real derivative. The comparison object is the finite product-rule expression: each hinge contributes an area factor times a deficit factor, differentiated by the product rule, then summed over hinges of the triangulation.
The filter relation $=^{\mathrm{f}}[\mathrm{nhds},0]$ means the two functions of $t$ coincide on some open neighborhood of the flat point $t=0$, which is the only regime needed for first-order tangency and Hessian extraction.
proof idea
No proof: the declaration is a Prop-valued definition. It packages the universal quantification over vertex potentials $\xi$ and the eventual equality, near $t=0$, between $\partial_t$ of the action along the line and the named product-rule derivative term. Discharge is left to later theorems that assume hinge/deficit line differentiability or a flat configuration.
why it matters
This target is the first-order product-rule checkpoint in the nonlinear Regge Hessian chain. It is discharged by the factor-differentiability theorem (each hinge line and each deficit line differentiable near the flat point) and, via that, by the flat-configuration theorem. The tangency theorem then consumes the product-rule target together with a quadratic-tangency hypothesis on the product-rule expression to conclude that the action derivative itself is tangent to the canonical quadratic form.
In the broader Recognition geometry stack this is scaffolding toward equating the nonlinear second directional derivative at flat potentials with the incidence Hessian, the exact endpoint named in the module header. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete-gravity calculus on a fixed triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.