local_conformal_schlaefli_cancellation
plain-language theorem explainer
On each tetrahedron of an incidence-consistent 3D triangulation, the six-edge weighted sum of edge lengths times the conformal chain-rule dihedral derivatives vanishes. Anyone proving first variation of the nonlinear Regge action at a conformal potential cites this local identity. The proof is finite-sum algebra: expand the chain rule, commute sums, and apply the already-proved per-tetrahedron Schläfli identity.
Claim. Let $K$ be an incidence-consistent 3D triangulation and $\eta$ a vertex potential on $K$. For every tetrahedron $\tau$, $$\sum_{f=1}^{6} \ell_f(\tau)\,(\partial_{\eta}\theta_f)^{\mathrm{chain}}(\tau)=0,$$ where $\ell_f=\sqrt{\mathrm{sqEdge}_f(\tau)}$ and $(\partial_{\eta}\theta_f)^{\mathrm{chain}}$ is the chain-rule directional derivative of the dihedral angle at face-edge $f$ through the six edge lengths under the conformal flow of $\eta$.
background
The module targets the first variation of the full nonlinear Regge action at a flat conformal potential. The geometric engine is classical Schläfli cancellation plus vanishing deficit: once per-tetrahedron weighted angle derivatives cancel, the remaining variation is controlled by hinge deficits.
A triangulation $K$ carries tetrahedra with six squared edge lengths each. Incidence consistency ensures the local Schläfli data package is well-defined. A vertex potential $\eta$ induces a conformal deformation of edge lengths; the local angle-length chain-rule derivative expands $d\theta_f$ as a linear combination of the six edge-length directional derivatives, with coefficients the partials of dihedral angle with respect to edge lengths.
The classical Schläfli differential identity on a single tetrahedron states $\sum_e \ell_e,d\theta_e=0$. That identity is already installed on the triangulation Schläfli data as the field schlaefli for each edge index $k$.
proof idea
Unfold the chain-rule derivative so the sum becomes a double sum over face-edges $f$ and edge indices $k$ of $\ell_f\cdot(\partial\theta_f/\partial\ell_k)\cdot(\partial_\eta\ell_k)$.
Commute the finite sums (mul_sum, sum_comm) and rearrange by ring to factor each edge-length directional derivative outside an inner sum $\sum_f \ell_f,(\partial\theta_f/\partial\ell_k)$.
For each fixed $k$, that inner sum is exactly the local Schläfli identity on tetrahedron $\tau$, hence zero. The outer sum of zeros is zero by simp. No analysis beyond the already-proved algebraic Schläfli field is used.
why it matters
This is the per-tetrahedron algebraic core of conformal Schläfli cancellation for the Regge first-variation program. Downstream, conformalSchlaefliCancellation_of_lengthChain_of_bookkeeping lifts the local identity through a length-chain package and incidence bookkeeping to a global statement. The Hessian module's ConformalSchlaefliAlongLineTarget records the strongest form: the weighted deficit-derivative sum vanishes along the entire conformal line, as the classical identity $\sum_{e\in\tau}\ell_e,d\theta_{e,\tau}=0$ applied at every parameter and summed over tetrahedra cancels the $\sum h\delta'$ term, leaving $S'(t)=\sum\delta h'$.
In the Recognition geometry stack this supplies the local cancellation step needed before global first-variation vanishing at the flat conformal potential. It does not itself touch the forcing chain (T0–T8) or constants; it is pure 3D Regge differential geometry supporting the action calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.