localEdgeLengthDirectionalDeriv
plain-language theorem explainer
Directional derivative of a tetrahedron edge length under a vertex-conformal potential equals the edge length times the average potential at its two endpoints. Cited by anyone building the length-to-angle chain rule for the first variation of the nonlinear Regge action. The body is an explicit algebraic formula from conformal scaling of squared edge lengths.
Claim. For a 3D triangulation $K$, vertex potential $\eta$, tetrahedron $\tau$, and edge index $f\in\{0,\ldots,5\}$, the directional derivative of the local edge length $\sqrt{a_f}$ along $\eta$ is $\sqrt{a_f}\cdot(\eta(u)+\eta(v))/2$, where $u,v$ are the two vertices of edge $f$ in tetrahedron $\tau$.
background
The module targets vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric route is Schläfli cancellation plus zero deficit; until the global derivative is fully expanded, local closed-form Schläfli data and named chain-rule factors are recorded explicitly.
A vertex potential $\eta$ is a real assignment to triangulation vertices, used as a conformal deformation direction. Each tetrahedron carries six squared edge lengths $a_f$. Under a conformal scaling, the directional derivative of squared length is proportional to $a_f$ times the sum of endpoint potentials, so the derivative of length $\sqrt{a_f}$ is $\sqrt{a_f}$ times the average endpoint potential.
Edge endpoints are recovered from the standard six-edge indexing of a tetrahedron (via the foundation edge-vertex map). Incidence-consistent triangulations and local Schläfli derivative tables sit upstream of the angle-side chain rule that consumes this factor.
proof idea
Pure definition, not a proved equality. Resolve the two endpoints of edge $f$ by the fixed tetrahedron edge-vertex table. Return the product of the current edge length $\sqrt{a_f}$ with the arithmetic mean of $\eta$ at those two vertices. No lemmas or tactics; the formula is the conformal chain-rule factor $d\sqrt{a}/d t = \sqrt{a},(\eta_u+\eta_v)/2$ written pointwise.
why it matters
This is the length leg of the local angle-length chain rule. Downstream, the angle derivative predicted by Schläfli data is the sum over edges of dihedral derivatives times this factor; that object is then shown equal to the squared-edge chain form, and the weighted sum of lengths times those angle derivatives cancels by the local Schläfli identity (local conformal Schläfli cancellation on one tetrahedron).
That local cancellation is the finite-sum engine behind the module goal: first variation of the nonlinear Regge action vanishes at the flat conformal potential. The same length-chain factor is reused in the gravity layer on the six-tetrahedron cubic Dirichlet/periodic Freudenthal instances, where mixed hinge-deficit targets expand into cell-tetrahedron length-chain sums. It does not itself invoke the forcing chain (T5–T8) or RCL; it is pure Regge calculus infrastructure for the discrete Einstein-Hilbert first variation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.