tetDihedralAngleUnderConformal_contDiffAt_zero
plain-language theorem explainer
At the flat (zero) vertex potential, each tetrahedral dihedral angle after conformal edge deformation is C^n-smooth for every extended order n, provided the undeformed Cayley–Menger dihedral cosine lies strictly in (-1,1). First-variation packages, deficit-angle smoothness, and the nonlinear Hessian line chart all cite this local fact. The proof composes the already-smooth conformal cosine with arccos, using the endpoint gap to keep arccos differentiable.
Claim. Let $K$ be a 3D triangulation, $\tau$ a tetrahedron index, and $f\in\{0,\ldots,5\}$ an edge of that tetrahedron. Let $\theta(\xi)$ be the dihedral angle at edge $f$ of tetrahedron $\tau$ after squared edge lengths are deformed by the conformal chart of a vertex potential $\xi$. If the Cayley–Menger dihedral cosine of the undeformed squared edges at $f$ is neither $-1$ nor $1$, then for every extended order $n\in\mathbb{N}\cup\{\infty\}$ the map $\xi\mapsto\theta(\xi)$ is $C^n$ at the zero potential.
background
This module records analytic inputs for the full nonlinear Regge action on a 3D triangulation. The closed second-order theory works with an exact quadratic truncation; the nonlinear theory needs the conformal edge chart inside the nondegenerate tetrahedral cone, arccos arguments away from $\pm 1$, and the finite Regge action smooth at the flat potential. Those requirements are named configuration hypotheses, not hidden axioms.
A vertex potential $\xi$ deforms squared edge lengths through the conformal chart. The dihedral cosine is the Cayley–Menger cofactor ratio (numerator a $3\times 3$ cofactor, denominator the associated edge factor). The dihedral angle is the arccos of that cosine. At the zero potential the conformal squared edges recover the original tetrahedron edges, so endpoint conditions on the undeformed cosine transfer directly.
Upstream geometry already supplies smoothness of the conformal dihedral cosine at zero, and Mathlib supplies $C^n$ regularity of $\arccos$ on $(-1,1)$.
proof idea
Unfold the conformal dihedral angle as $\arccos$ of the conformal Cayley–Menger cosine. Invoke the existing lemma that this cosine map is $C^n$ at the zero potential. Rewrite the two endpoint inequalities through the identity that conformal squared edges at zero equal the original squared edges, so the cosine value at zero still avoids $\pm 1$. Apply Mathlib’s $\operatorname{ContDiffAt}$ fact for $\arccos$ at that interior value, then compose the two $\operatorname{ContDiffAt}$ maps (cosine then arccos) at the zero potential.
why it matters
Local $C^n$ regularity of each conformal dihedral angle at the flat chart is a brick in the nonlinear Regge calculus stack. It is used by the deficit-angle smoothness theorem (deficit as a sum of dihedrals), by the first-variation package that defines directional derivatives of dihedral angles along line potentials at a flat configuration, and by the line-restricted ContDiff input to the nonlinear Hessian proof.
In the Recognition geometry layer this keeps the discrete curvature functional analytic enough for variational calculus on 3D triangulations, aligned with the forced spatial dimension $D=3$ (forcing step T8) and with treating flat configurations as the natural expansion point. The module’s role is to expose these analytic gates explicitly rather than bury them as axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.