ProductRuleTangencyToQuadraticTarget
plain-language theorem explainer
Target property: along every conformal line through a vertex potential, the product-rule Regge-action derivative is first-order tangent at t=0 to the derivative of the canonical quadratic. Downstream lemmas cite it to reduce full action-derivative tangency to a product-rule-plus-Hessian match. It is a Prop definition, not a proved statement.
Claim. For an incidence-consistent finite 3D triangulation $K$ and every vertex conformal potential $\xi$, the real map $t \mapsto D_{\mathrm{prod}}(K,\xi;t) - \frac{d}{dt}Q(K,\xi;t)$ has derivative $0$ at $t=0$, where $D_{\mathrm{prod}}$ is the product-rule expression for the Regge action derivative along the conformal line through $\xi$, and $Q$ is the canonical quadratic form restricted to that line.
background
The module isolates the remaining hard step for the full nonlinear Regge Hessian: the second directional derivative of the action at the flat potential must equal the canonical incidence Hessian. Once that chain-rule calculation is in place, the existing second-variation input package follows at once.
A finite 3D triangulation carries abstract incidence data and nondegenerate squared-edge lengths on each tetrahedron. Vertex conformal potentials are real assignments to vertices; the conformal line through a potential $\xi$ scales that assignment by a real parameter $t$. The canonical quadratic along the line is half the Hessian quadratic form of the canonical Regge Hessian evaluated on the line potential. The product-rule derivative is the exact finite-sum expression obtained by differentiating the hinge factor and the deficit factor of the Regge action along that line.
The present target packages the residual geometric claim after the product-rule expression is available: that expression must be first-order tangent at zero to the derivative of the canonical quadratic.
proof idea
Definition of a Prop, not a theorem. The body is a universal quantification over vertex potentials $\xi$, asserting HasDerivAt at $0$ with value $0$ for the difference of the product-rule derivative and the ordinary derivative of the canonical quadratic along the line. No tactics or lemmas are applied here; discharge is deferred to the sibling that assumes the product-rule derivative matches the canonical Hessian.
why it matters
This is the geometric linearization step that sits between the product-rule expansion of the Regge action and full first-order tangency of the true action derivative to the canonical quadratic. The parent actionDerivativeTangencyToQuadratic_of_productRule combines a near-zero product-rule hypothesis with this target to obtain action-derivative tangency. The sibling productRuleTangencyToQuadratic_of_productRuleDerivativeCanonicalHessian shows the target follows once the product-rule derivative is identified with the canonical Hessian (using second-differentiability of the canonical quadratic at zero).
In the module's program, that tangency is the last link needed so the second directional derivative at the flat potential equals the canonical incidence Hessian, closing the nonlinear Regge second-variation interface. It is scaffolding for the Hessian match, not a new physical assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.