localAngleLengthChainDeriv_eq_sqEdgeChainDeriv
plain-language theorem explainer
On an incidence-consistent 3D triangulation, the local chain-rule derivative of dihedral angles along a conformal length direction equals the same derivative routed through squared edge lengths. First-variation arguments for the nonlinear Regge action cite this to switch presentations freely. The proof is termwise finite-sum congruence plus square-root algebra relating the two directional factors.
Claim. Let $K$ be an incidence-consistent 3D triangulation, $\eta$ a vertex potential, $\tau$ a tetrahedron index, and $f\in\{0,\ldots,5\}$ an edge index of that tetrahedron. Then the local conformal chain-rule derivative of the dihedral data through edge lengths equals the local conformal chain-rule derivative through squared edge lengths: $\partial^{\mathrm{conf}}_{\mathrm{length}}\theta_{\tau,f}(\eta)=\partial^{\mathrm{conf}}_{\mathrm{sq}}\theta_{\tau,f}(\eta)$.
background
The module targets the first variation of the nonlinear Regge action on a 3D triangulation, aiming at vanishing at the flat conformal potential by Schläfli cancellation plus zero deficit.
Each tetrahedron carries six positive squared edge lengths. Incidence consistency glues local edge and hinge data into a global complex. A vertex potential assigns a real number to each vertex; the conformal direction deforms an edge by the sum of the potentials at its endpoints (equivalently, deforms squared lengths).
Two local chain derivatives are defined on a single tetrahedron: one multiplies closed dihedral derivatives by length directional derivatives, the other by squared-edge directional derivatives, then sums over the six edges. Schläfli data extracted from the incidence-consistent triangulation supply the closed dihedral-versus-length factors used on the length side.
proof idea
Unfold both chain derivatives and apply Finset.sum_congr to reduce to a termwise identity over edges $k$. For each $k$, the dihedral derivative stored in the incidence-consistent Schläfli package equals the closed length-form dihedral derivative by definitional rfl.
Unfold the length directional derivative, the conformal squared-edge directional derivative, and the closed dihedral-length formula. With $s_k$ the squared edge length (strictly positive), the identity $\sqrt{s_k}\cdot\sqrt{s_k}=s_k$ (equivalently $\sqrt{s_k}^2=s_k$) converts the length-side chain factor into the squared-edge factor after mul_assoc and ring_nf. A final ring finishes the algebraic match.
why it matters
Downstream, localAngleLengthChainRulePackage_of_sqEdge builds a length-based chain-rule package from a squared-edge package by invoking this equality. Classical Schläfli and Regge first-variation statements are phrased in lengths; conformal smoothness and directional calculus are cleaner in squared edges. Equating the two lets the module keep both presentations.
The parent goal is vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. Once local length and squared-edge chain rules agree, local Schläfli cancellation on each tetrahedron feeds the global deficit-weighted sum. In the Recognition geometry layer this is discrete curvature bookkeeping on 3D triangulations, aligned with the forced spatial dimension $D=3$ (T8) that makes tetrahedral Regge calculus the native setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.