localAngleSqEdgeChainDeriv
plain-language theorem explainer
Chain-rule first derivative of a tetrahedron dihedral angle along a conformal vertex potential, written in squared-edge coordinates. Anyone assembling the first variation of the nonlinear Regge action at the flat potential cites this scalar. It is the explicit six-term sum of closed-form dihedral cofactors times conformal edge stretch rates. Pure definitional abbreviation of that sum.
Claim. For a finite 3D Regge triangulation $K$, vertex conformal potential $\eta$, tetrahedron index $\tau$, and local edge $f\in\{0,\ldots,5\}$, the squared-edge chain derivative of the local dihedral angle is $\sum_{k=0}^{5}(\partial_{\ell_k^2}\theta_f)\,D_\eta(\ell_k^2)$, where $\partial_{\ell_k^2}\theta_f$ is the closed-form dihedral derivative in squared-edge coordinates and $D_\eta(\ell_k^2)$ is the directional derivative of the $k$-th conformal squared edge at the flat potential.
background
The module targets vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric engine is Schläfli cancellation plus zero deficit; this file records the analytic chain-rule scaffolding until the closed-form local Schläfli identities are fully expanded.
A Triangulation3D is a finite abstract 3D Regge complex with nondegenerate squared-edge data on every tetrahedron. A vertex conformal potential is a real assignment to vertices; the flat (zero) potential is the expansion point. Each tetrahedron carries six squared-edge coordinates.
Upstream, dihedralClosedDerivSq supplies the closed-form value of $\partial\theta_e/\partial\ell_k^2$ on a nondegenerate tetrahedron. Separately, conformalLocalSqEdgeDirectionalDeriv is the directional derivative of a local conformal squared edge at the flat potential: $\ell_f^2,(\eta_u+\eta_v)$ for the two endpoints of edge $f$. The present definition multiplies those two ingredients and sums over the six edges.
proof idea
Definitional one-liner. Expand as the finite sum over the six local edge indices $k$ of the product
dihedralClosedDerivSq (K.tet τ) f k * conformalLocalSqEdgeDirectionalDeriv K η τ k.
No tactics, no lemmas applied beyond the two named upstream scalars. The sum is exactly the multivariable chain rule for $\theta_f$ as a function of the six squared edges, each of which is stretched by the conformal line through $\eta$.
why it matters
This scalar is the squared-edge avatar of the local angle derivative used throughout the first-variation calculation. Downstream, localAngleLengthChainDeriv_eq_sqEdgeChainDeriv proves it coincides with the length-coordinate chain derivative (under incidence consistency), so either coordinate chart may be used. It is also the derivative value packaged into LocalAngleSqEdgeChainRulePackage and discharged at the flat configuration by localAngleSqEdgeChainRulePackage_of_flat, which asserts HasDerivAt for each tetrahedron dihedral angle along the conformal line.
In the broader Recognition geometry stack this sits inside the analytic half of the Regge first-variation argument: once every local angle derivative is under control, Schläfli cancellation plus vanishing deficit at the flat conformal potential yields the global first variation zero. That is the geometric input needed before curvature and action identities are matched to the forcing-chain landmarks (eight-tick structure, $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.