localAngleSqEdgeChainRulePackage_of_flat
plain-language theorem explainer
Under a flat, incidence-consistent 3D triangulation, every local dihedral angle along a conformal line deformation of a vertex potential is differentiable at t=0, with derivative equal to the squared-edge chain-rule formula. Analysts of the nonlinear Regge first variation cite this package as the angle half of the Schläfli input. The body is a chain-rule assembly: fderiv of arccos-dihedral composed with the conformal squared-edge path, evaluated via coordinate singles.
Claim. Let $K$ be a 3D triangulation that is incidence-consistent and flat. Then the local squared-edge chain-rule package holds: for every vertex potential $\eta$, tetrahedron index $\tau$, and face-pair index $f\in\{0,\ldots,5\}$, the map $t\mapsto$ (dihedral angle of tet $\tau$ on hinge $f$ under the conformal deformation along $\eta$ at time $t$) has derivative at $t=0$ equal to the explicit local squared-edge chain derivative.
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 inputs until closed-form local Schläfli identities are fully expanded.
Squared edge lengths of a tetrahedron are the type SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). Dihedral angles are recovered from Cayley–Menger data via dihedralAngle3Sq / dihedralCos3Sq. A conformal line potential deforms vertex values linearly in $t$; the induced squared-edge path and its directional derivative at $t=0$ are already available from the smoothness layer.
LocalAngleSqEdgeChainRulePackage packages the squared-edge chain-rule form that follows from the explicit cofactor/arccos coordinate derivatives: each local dihedral angle under the conformal line has a named derivative at the flat basepoint.
proof idea
Fix potential $\eta$, tet $\tau$, and hinge $f$. Let $F$ be dihedral angle as a function of squared edges, and let $v$ be the conformal squared-edge directional derivative at $t=0$. Flatness supplies the arccos endpoint condition ($\cos\neq\pm 1$), so $F$ is $C^1$ (hence differentiable) at the base squared-edge vector by dihedralAngle3Sq_contDiffAt_nonDegenerate.
The conformal tet squared-edge path has derivative $v$ at $0$ (conformalTetSqEdges_hasDerivAt_line_zero), and at $t=0$ it recovers the geometric edges. Compose HasFDerivAt of $F$ with that path derivative. Expand the Fréchet derivative on $v$ as a sum over the six edge slots via continuousLinearMap_apply_eq_sum_single, identify each coordinate derivative with fderiv_dihedralAngle3Sq_apply_single, and match the packaged chain derivative. Rewrite to the conformal dihedral angle path.
why it matters
This definition is the angle-side analytic input for the Regge first-variation pipeline. Downstream, reggeActionFirstVariationInput_of_incidenceBookkeeping and reggeActionFirstVariationInput_of_edgeSlotBookkeeping thread it (via length-chain and incidence bookkeeping) into the full first-variation input at a flat configuration. The gravity instance canonicalPeriodicLocalAngleLengthChainRulePackage builds the analogous length-chain package on the periodic Freudenthal torus, so this flat squared-edge package is the local model those global constructions mirror.
In the module narrative, first variation vanishes by Schläfli cancellation plus zero deficit at the flat conformal potential. Packaging differentiability of local angles under conformal edge motion is the precise analytic step that lets the discrete Schläfli identity become a derivative identity. It does not itself invoke the Recognition forcing chain (T5–T8) or the mass ladder; it is pure discrete geometry supporting the Regge/gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.