dihedralAngle3SqClosedFormDeriv
plain-language theorem explainer
Closed-form partial of a tetrahedral dihedral angle w.r.t. one squared edge length, via the arccos chain rule on the Cayley–Menger cofactor cosine. Cited by anyone differentiating Regge action or Schläfli identities in squared-edge coordinates. The body is the standard calculus multiplier times the already-computed cosine derivative; no extra algebra lives here.
Claim. For squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$, hinge edge $e$, and coordinate index $k$, the closed-form dihedral-angle derivative is $$-\frac{1}{\sqrt{1-\cos^2\theta_e(a)}}\,\partial_k\cos\theta_e(a),$$ where $\cos\theta_e(a)$ is the Cayley–Menger cofactor-ratio cosine and $\partial_k\cos\theta_e(a)$ is its closed-form coordinate derivative.
background
This module isolates the analytic half of tetrahedral dihedral derivatives. Once the cosine is known as a function of the six squared edge lengths, the angle is $\theta=\arccos(\cos\theta)$, so
$$d\theta=-(1/\sqrt{1-\cos^2\theta}),d(\cos\theta).$$
Squared edges are the type SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The cosine dihedralCos3Sq is the ratio of a $3\times3$ Cayley–Menger cofactor to a positive denominator built from the two face cofactors opposite the hinge. Its closed-form partials live one layer down as dihedralCos3SqClosedFormDeriv (quotient rule on numerator and denominator cofactor derivatives).
The hard geometric work is therefore already done upstream; this definition only packages the arccos multiplier that the calculus interface must feed to Regge and Schläfli arguments.
proof idea
Pure definition, not a proof. The value is written as the product of the standard arccos chain-rule factor $-(1/\sqrt{1-c^2})$ evaluated at $c=\mathrm{dihedralCos3Sq}(a,e)$ with the upstream closed-form cosine partial dihedralCos3SqClosedFormDeriv a e k. The companion theorem dihedralAngle3SqClosedFormDeriv_def is rfl and records the equality for rewriting.
why it matters
Supplies the explicit scalar that hasDerivAt_dihedralAngle3Sq_explicit claims is the true coordinate derivative of the cofactor-defined dihedral angle. Downstream, Schläfli proofs (dihedralClosedDerivSq, dihedralClosedDerivSq_eq_poly) and the nonlinear Regge Hessian layer consume it: LocalConformalSchlaefliAngleSqEdgeChainRuleNearZeroTarget requires that each local dihedral derivative equal this closed-form squared-edge gradient paired with the conformal edge velocities, and the gluing theorem localConformalSchlaefliNearZero_of_sqEdgeChainRule_and_closedFormZero combines that chain rule with the algebraic Schläfli zero. In the broader Recognition geometry stack this is the calculus bridge from Cayley–Menger algebra to first-order Regge variation in $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.