dihedralDenom3_contDiffAt_nonDegenerate
plain-language theorem explainer
At any non-degenerate tetrahedron, the dihedral denominator (square root of the product of the two opposite Cayley–Menger diagonal cofactors for a chosen edge) is C^n-smooth in the six squared edge lengths, for every extended order n. Regge-calculus analysts cite this when differentiating hinge angles against edge lengths. The argument multiplies two globally smooth cofactors and takes a square root at a strictly nonzero value.
Claim. Let $T$ be a non-degenerate tetrahedron with squared edge lengths $a_T\in\mathbb{R}^6$. Fix an edge index $f\in\{0,\ldots,5\}$ and an order $n\in\mathbb{N}\cup\{\infty\}$. The real-valued map sending squared edge lengths $a$ to the dihedral denominator of edge $f$ (the square root of the product of the two opposite Cayley–Menger diagonal cofactors) is $C^n$ at the point $a_T$.
background
This module sets up the analytic side of the first variation of the full nonlinear Regge action. The geometric target is Schläfli cancellation plus zero deficit at the flat conformal potential; the present file records the exact smoothness and derivative statements needed before that cancellation is expanded.
Squared edge lengths of a tetrahedron are packaged as a map $a:\mathrm{Fin},6\to\mathbb{R}$. From them one builds the Cayley–Menger matrix and its cofactors $C_{r,c}$. Every such cofactor is globally $C^n$ in the six squared lengths (the theorem cmCofactor3_contDiff). The dihedral denominator for edge $f$ is the square root of the product of the two diagonal cofactors at the pair of vertices opposite that edge.
Non-degeneracy of $T$ is the standing hypothesis that keeps those denominators away from zero, via the polynomial identity equating the denominator to an explicit Cayley–Menger polynomial that does not vanish on non-degenerate tets.
proof idea
Unfold the denominator as $\sqrt{C_{pp}C_{qq}}$ for the opposite vertex pair $(p,q)$ of edge $f$. Global smoothness of each cofactor specializes to ContDiffAt at $T$'s squared edges; the product of those two maps is therefore ContDiffAt. Non-vanishing of the denominator at $T$ is rewritten, via the cofactor–polynomial identity, as non-vanishing of the associated polynomial on non-degenerate tets; that forces the product of cofactors itself to be nonzero at $T$. The square-root lemma for ContDiffAt then closes the argument.
why it matters
Smoothness of the dihedral denominator is the first link in the local smoothness chain for hinge geometry: the immediate consumer is smoothness of the squared cosine of the dihedral angle at the same non-degenerate point, which in turn feeds smoothness of the dihedral angle itself and the directional derivatives of hinge measures.
Those derivatives are the analytic input to the first variation of the nonlinear Regge action. The module's target is vanishing of that variation at the flat conformal potential by Schläfli cancellation plus zero deficit. Establishing $C^n$ control on the denominator removes the main singularity obstruction before the closed-form local Schläfli identities are differentiated.
In the broader Recognition geometry stack this sits under the discrete curvature / Regge side that supports continuum limits in three spatial dimensions (forcing landmark T8), not under the J-cost or phi-ladder arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.