actionDerivativeProductRuleNearZero_of_flatConfiguration
plain-language theorem explainer
For an incidence-consistent 3D triangulation with a flat analytic configuration, the first derivative of the nonlinear Regge action along any vertex-potential line equals, near the origin, the finite product-rule sum of hinge and deficit derivatives. Second-variation arguments that match the action to the canonical incidence Hessian cite this step. The proof is a one-line term application of the factor-differentiability product rule, fed by flat-configuration hinge/deficit line differentiability.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation admitting a flat analytic configuration. Then for every vertex potential $\xi$, $$t \mapsto \partial_t\,S(t\xi)$$ agrees in a neighborhood of $t=0$ with the finite product-rule derivative built from hinge-length derivatives and deficit-angle derivatives along that line.
background
This module isolates the hard endpoint of the nonlinear Regge second-variation chain: at a flat potential, the second directional derivative of the full action must equal the canonical incidence Hessian. The local objects are a finite 3D triangulation $K$ with incidence consistency, vertex potentials $\xi$, and the action restricted to the real line $t\mapsto S(t\xi)$.
A flat analytic configuration packages three facts: arccos endpoints stay interior (dihedral cosines squared avoid $\pm 1$), all hinge deficits vanish at the base point, and the nonlinear action is smooth enough for Taylor calculus. The product-rule target asserts that near $t=0$ the ordinary derivative of the action along the line equals a finite sum of hinge-derivative and deficit-derivative terms (the explicit product rule for the Regge sum).
Upstream, factor differentiability of every hinge line and every deficit line near zero is already enough to discharge that target. Flatness supplies exactly that joint differentiability package.
proof idea
One-line term proof. Apply the general lemma that hinge/deficit line differentiability near zero implies the product-rule target, and feed it the specialization of that differentiability hypothesis to a flat configuration. No extra algebraic work occurs at this node.
why it matters
This is a bridge lemma inside the nonlinear Hessian interface, not a new physical assumption. It converts geometric flatness into the first-derivative product-rule identity needed before second derivatives are compared to the canonical incidence Hessian.
Downstream it is consumed by the tangency theorem that, given also the product-rule derivative matching the canonical Hessian, concludes first-order tangency of the action derivative to the quadratic model along every line. That tangency is the exact endpoint the module doc names: once supplied, the existing second-variation input for the nonlinear Regge action follows immediately. In the broader Recognition geometry stack this is the analytic step that lets discrete curvature (Regge deficits on a 3D complex) recover the expected quadratic Hessian at flat space, consistent with the $D=3$ forcing landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.