dihedralAngle3Sq_contDiffAt_nonDegenerate
plain-language theorem explainer
At any nondegenerate tetrahedron whose dihedral cosine on edge f lies strictly inside (-1,1), the map sending the six squared edge lengths to that dihedral angle is C^n-smooth for every extended natural n. Analysts of the nonlinear Regge action cite this to justify Fréchet and directional derivatives of hinge angles. The proof is composition of the already-smooth cosine map with arccos, which is smooth off the endpoints ±1.
Claim. Let $T$ be a nondegenerate tetrahedron and $f\in\{0,\ldots,5\}$ an edge index. Write $a_T$ for its six squared edge lengths and $\cos\theta_f(a)$ for the Cayley–Menger dihedral cosine on edge $f$. If $\cos\theta_f(a_T)\notin\{-1,1\}$, then for every extended order $n\in\mathbb{N}\cup\{\infty\}$ the map $a\mapsto\theta_f(a):=\arccos(\cos\theta_f(a))$ is $C^n$ at $a_T$.
background
This module targets the vanishing of the first variation of the full nonlinear Regge action at a flat conformal potential. The geometric engine is Schläfli cancellation plus zero deficit; the analytic work is to make every local dihedral angle a differentiable (in fact $C^n$) function of the six squared edge lengths so that Fréchet and directional derivatives exist.
Squared edge data live in SqEdges $:= \mathrm{Fin},6\to\mathbb{R}$. The cosine $\mathrm{dihedralCos3Sq}(a,e)$ is the ratio of a Cayley–Menger $3\times3$ cofactor to a denominator built from the same polynomial; the angle is then $\arccos$ of that cosine. Nondegeneracy of $T$ keeps volumes and denominators nonzero, but arccos still requires the cosine to avoid the branch points $\pm1$.
A sibling result already gives $C^n$ smoothness of the cosine map at $T$. The present statement lifts that to the angle by composing with arccos on the open interval $(-1,1)$.
proof idea
Unfold the angle as $\arccos\circ\mathrm{dihedralCos3Sq}(\cdot,f)$. Invoke the sibling lemma that the cosine is $\mathrm{ContDiffAt},\mathbb{R},n$ at $T.\mathrm{sqEdge}$. Separately, $\mathrm{Real.contDiffAt_arccos}$ supplies $C^n$ smoothness of arccos at the value $\mathrm{dihedralCos3Sq}(T.\mathrm{sqEdge},f)$, using the two endpoint inequalities. Finish by $\mathrm{ContDiffAt.comp}$ and a simpa that rewrites function composition.
why it matters
Without $C^n$ control on each local dihedral angle, the first-variation and Hessian pipelines for the nonlinear Regge action cannot even state their chain-rule packages. Immediate consumers include the single-coordinate Fréchet evaluation fderiv_dihedralAngle3Sq_apply_single, the flat local angle–edge chain-rule package, and the near-zero conformal Schläfli chain rule used in the nonlinear Hessian proof.
On the gravity side the same lemma feeds the TT derivative gate (directional derivative of a flat angle along an affine squared-edge path), the flat second-variation directional derivative at an arbitrary nondegenerate tet, and plane-wave amplitude smoothness of tetrahedral dihedral angles. In the Recognition geometry stack this is the analytic gate that lets Schläfli identities become variational identities for the discrete action, supporting the D=3 Regge sector of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.