localAngleLengthChainRulePackage_of_sqEdge
plain-language theorem explainer
Converts a squared-edge local dihedral chain-rule package into the edge-length form required by the Regge first-variation input, on any incidence-consistent 3D triangulation. Anyone wiring cofactor/arccos angle derivatives into the nonlinear Regge variation cites this bridge. The body is a one-line rewrite: the two closed-form chain derivatives agree, so the existing HasDerivAt proof transfers.
Claim. Let $K$ be a 3D triangulation that is incidence-consistent. Suppose one is given, for every vertex potential $\eta$, tetrahedron $\tau$, and face index $f$, a proof that the conformal dihedral angle $t\mapsto\theta_\tau^f(\eta+t\cdot\mathbf{1})$ is differentiable at $t=0$ with derivative equal to the squared-edge chain-rule expression. Then the same maps are differentiable at $0$ with derivative equal to the edge-length chain-rule expression, yielding a local angle-length chain-rule package on $K$.
background
This module targets the 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; the analytic obligation is to control directional derivatives of tetrahedral dihedral angles under conformal vertex potentials.
A conformal line potential deforms edge lengths by scaling from vertex values. Two closed-form expressions for the $t=0$ derivative of a dihedral angle are in play: the squared-edge chain rule (native to cofactor/arccos coordinate formulas) and the edge-length chain rule (the form demanded by the global first-variation bookkeeping). The structure LocalAngleSqEdgeChainRulePackage packages the former HasDerivAt statements; LocalAngleLengthChainRulePackage packages the latter and still requires incidence consistency on $K$.
Upstream, the equality theorem identifies the two scalar derivative expressions pointwise, so the packages differ only in which expression is named as the derivative target.
proof idea
One-line package conversion. For each vertex potential, tetrahedron, and face slot, pull the squared-edge HasDerivAt witness from the input package. Rewrite the claimed derivative value by the pointwise identity that the edge-length chain derivative equals the squared-edge chain derivative (under incidence consistency). The rewritten goal matches the input witness exactly.
why it matters
The length-form package is the local analytic input consumed when assembling ReggeActionFirstVariationInput from incidence or edge-slot bookkeeping. Downstream constructors thread this conversion under a conformal Schläfli incidence bookkeeping hypothesis, then feed the resulting first-variation input into the vanishing theorem for the nonlinear Regge action at flat configurations.
It is also the return type of the canonical periodic package on the Freudenthal torus used by the physical six-tetrahedra cubic Dirichlet instance, so concrete gravity models inherit the length-form interface through this bridge.
Within the Recognition geometry stack this sits under the $D=3$ triangulation layer (forcing chain T8) and supplies the derivative bookkeeping needed before Schläfli cancellation can cancel the first variation. It does not itself prove any angle derivative; it only renames the target once the squared-edge formulas are already established.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.