localAngleLengthChainDeriv
plain-language theorem explainer
Local dihedral-angle derivative along a conformal vertex-potential direction, formed by chaining closed Schläfli dihedral Jacobians against edge-length directional derivatives on one tetrahedron. First-variation and Schläfli-cancellation arguments for the nonlinear Regge action cite it as the explicit length-chain value. The body is a six-term sum of products of precomputed dihedral derivatives and local edge-length derivatives.
Claim. For an incidence-consistent finite 3D Regge triangulation $K$, a vertex conformal potential $\eta$, a tetrahedron index $\tau$, and a local edge slot $f\in\{0,\ldots,5\}$, define $$\sum_{k=0}^{5}(\partial_k\theta_f)(\tau)\cdot D_\eta\ell_k(\tau),$$ where $\partial_k\theta_f$ is the closed-form Schläfli partial of the dihedral angle at slot $f$ with respect to edge $k$, and $D_\eta\ell_k$ is the directional derivative of the local edge length $\sqrt{a_k}$ under the conformal deformation induced by $\eta$.
background
This module targets the 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 full derivative is expanded from closed-form local Schläfli identities, the module records exact analytic statements and named inputs.
A Triangulation3D is a finite abstract 3D Regge complex with nondegenerate squared-edge data on every tetrahedron. A vertex conformal potential is a real function on the vertices. Incidence consistency supplies global squared edges, local-to-global edge matching, and the local closed-form Schläfli data used here via triangulationSchlaefliData_of_incidence.
The upstream edge-length factor is the directional derivative of $\sqrt{a_f}$ under a vertex-conformal direction: $\sqrt{a_f}$ times the average of the potential values at the two endpoints of the local edge. The dihedral factors come from the already-proved local Schläfli derivative table on each tetrahedron.
proof idea
Definition, not a proved theorem. The value is the finite sum over the six local edge slots $k$ of
(dihedralDeriv f k) * localEdgeLengthDirectionalDeriv K η τ k,
where dihedralDeriv is read from the tetrahedron Schläfli data built from incidence consistency, and the second factor is the conformal edge-length directional derivative already defined in this module. No tactics or lemmas are applied beyond that lookup and multiplication.
why it matters
Supplies the explicit length-chain angle derivative used throughout the first-variation scaffold. Downstream, it is identified with the squared-edge chain form (localAngleLengthChainDeriv_eq_sqEdgeChainDeriv), packaged as the value field of LocalAngleLengthChainRulePackage (whose remaining obligation is HasDerivAt for the actual arccos/cofactor angle), and fed into local_conformal_schlaefli_cancellation, the pure finite-sum identity
$\sum_f \sqrt{a_f},(\text{this quantity})_f = 0$
on each tetrahedron.
That local cancellation is the analytic core of the module target: first variation of the nonlinear Regge action at the flat conformal potential. Gravity-side six-tet cubic Dirichlet instances reuse the same length-chain angle values in mixed hinge-deficit stencil targets on the periodic Freudenthal torus. In the broader RS geometry stack this is the local differential input that lets Schläfli cancel conformal length variations before global deficit bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.