LocalAngleSqEdgeChainRulePackage
plain-language theorem explainer
Packages the squared-edge chain rule for local dihedral angles under conformal vertex-potential deformations of a 3D triangulation. Cited by anyone assembling the first variation of the nonlinear Regge action at the flat potential. The structure records only the differentiability claim at t=0 with the explicit cofactor/arccos derivative; constructors supply the proof.
Claim. For a 3D triangulation $K$, a squared-edge local-angle chain-rule package is the assertion that for every vertex-potential direction $\eta$, tetrahedron $\tau$, and local edge index $f\in\{0,\ldots,5\}$, the real map $t\mapsto$ (dihedral angle of edge $f$ in $\tau$ under the conformal squared-edge data of the line potential $t\eta$) is differentiable at $t=0$, with derivative equal to $\sum_{k=0}^{5}(\partial\theta_f/\partial s_k)\,D_k\eta$, the closed-form chain rule in squared-edge coordinates.
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; until the global derivative is expanded from closed-form local Schläfli identities, the module records exact analytic packages for the local pieces.
A vertex potential assigns a real scalar to each vertex. The line potential through the flat configuration in direction $\eta$ is the ray $t\mapsto t\eta$. Under the conformal ansatz, squared edge lengths of each tetrahedron are determined by those vertex values; the local dihedral angle is then read off by the Cayley-Menger cofactor formula (arccos of a rational function of the six squared edges).
The companion quantity localAngleSqEdgeChainDeriv is the explicit first-order formula obtained by differentiating that arccos/cofactor expression and contracting against the directional derivatives of the six local squared edges. This structure packages the claim that the geometric angle map really has that derivative at $t=0$.
proof idea
No proof body: the declaration is a structure whose single field is the universal differentiability statement. Inhabitants are built downstream. The flat-configuration constructor discharges the field by specializing the already-proved continuous differentiability of the squared-edge dihedral-angle map at nondegenerate data and evaluating the Fréchet derivative on the line direction. The length-form converter simply rewrites the same derivative via the chain rule relating edge lengths to squared edges, under an incidence-consistency hypothesis.
why it matters
This package is the squared-edge intermediate step between the closed-form local Schläfli identities and the length-coordinate first-variation statement needed for the Regge action. Downstream, localAngleSqEdgeChainRulePackage_of_flat produces an instance on any flat configuration, and localAngleLengthChainRulePackage_of_sqEdge converts it into the length-form package used by the global first-variation argument.
In the Recognition geometry stack the first variation must vanish at the flat conformal potential (Schläfli cancellation plus zero deficit). Recording the local angle derivatives in squared-edge coordinates keeps the analytic hypotheses aligned with the Cayley-Menger formulas already proved for tetrahedra, before any change of variables to edge lengths. The structure therefore sits on the critical path from local 3D Schläfli identities to the vanishing of $\delta S_{\mathrm{Regge}}$ at flat space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.