dihedralCos3Sq_contDiffAt_nonDegenerate
plain-language theorem explainer
The cosine of each dihedral angle of a nondegenerate tetrahedron, as a function of the six squared edge lengths, is C^n-smooth at that tetrahedron for every n (including infinity). Anyone differentiating Regge dihedral data or the nonlinear Regge action with respect to edges cites this. The proof is a ContDiffAt quotient: smooth Cayley-Menger cofactor over a nonvanishing smooth denominator on the nondegenerate locus.
Claim. Let $T$ be a nondegenerate tetrahedron with squared edge lengths $a_T\in\mathbb{R}^6$, fix an edge index $f\in\{0,\ldots,5\}$, and let $n\in\mathbb{N}\cup\{\infty\}$. Then the map sending squared edge lengths $a$ to the cosine of the dihedral angle associated to edge $f$ is of class $C^n$ at $a_T$.
background
This module targets 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 work is to justify differentiating dihedral data in squared edge lengths.
Squared edge lengths live in $\mathrm{SqEdges}\simeq\mathbb{R}^6$. Dihedral cosines are realized via Cayley-Menger cofactors: the numerator is a signed $3\times 3$ minor cofactor $C_{p,q}$ of the $5\times 5$ Cayley-Menger matrix, and the denominator is a related cofactor expression that vanishes only on degenerate configurations. Upstream, every Cayley-Menger cofactor is globally $C^\infty$ in the six squared edges. A sibling lemma already gives ContDiffAt for the denominator on nondegenerate tetrahedra, and a cofactor-derivative identity identifies that denominator with a polynomial known to be nonzero off the degenerate locus.
proof idea
Unfold the cosine as numerator over denominator. The numerator is a fixed Cayley-Menger cofactor, hence ContDiffAt by the global smoothness theorem for cofactors (restricted to a point). The denominator is ContDiffAt by the sibling nondegenerate-denominator lemma. Nonvanishing of the denominator at $T$ follows by rewriting it as the cofactor polynomial and invoking the nondegeneracy nonvanishing lemma. ContDiffAt of the quotient then follows from the standard division rule for ContDiffAt maps with nonzero denominator. A final simp aligns the opposite-vertex indices.
why it matters
This is the cosine half of the smoothness ladder needed before one can differentiate dihedral angles themselves. The sole direct consumer is the companion theorem that the dihedral angle (arccos of this cosine) is ContDiffAt on the nondegenerate locus away from the endpoints $\pm 1$. That angle smoothness feeds directional derivatives of hinge measures and, ultimately, the first-variation identity for the nonlinear Regge action at flat conformal potential (Schläfli cancellation plus zero deficit). In the Recognition geometry stack it is pure analytic infrastructure: no new physical constant is fixed here, but without it the Regge variation cannot be stated as a classical derivative on edge space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.