dihedralCos3Sq_conformal_contDiffAt_zero
plain-language theorem explainer
Squared dihedral cosine of any tetrahedron edge, pulled back through the conformal squared-edge chart, is C^n at the zero vertex potential for every extended order n. Discrete-geometry and Regge-calculus workers cite it when promoting the flat-background quadratic truncation to a smooth nonlinear action. The proof unfolds the Cayley–Menger quotient and divides two already-smooth cofactor maps, using nonvanishing of the denominator at the flat point.
Claim. Fix a 3D triangulation $K$, a tetrahedron $\tau$, an edge index $f\in\{0,\ldots,5\}$, and an extended smoothness order $n\in\mathbb{N}\cup\{\infty\}$. The map sending a vertex potential $\xi$ to the Cayley–Menger squared dihedral cosine of edge $f$ on the conformally deformed squared edge lengths of $\tau$ is $C^n$ as a real function of $\xi$ at the zero potential.
background
The module supplies analytic hypotheses for the full nonlinear Regge action: the conformal edge chart must remain inside the nondegenerate tetrahedral cone, arccos arguments must stay off $\pm 1$, and the finite action must be smooth at the flat potential. Those requirements are packaged as named configuration facts rather than axioms.
Squared edge data live in SqEdges. The Cayley–Menger dihedral cosine of an edge is the quotient of an off-diagonal 3-cofactor by the geometric mean of the two corresponding diagonal cofactors (the denominator). Conformal deformation multiplies squared edge lengths by vertex-potential factors; at the zero potential the deformed edges recover the background tetrahedron.
Upstream, the numerator cofactor and the denominator are already known to be $C^n$ at zero under the same conformal chart, and the local denominator is nonzero on every background tetrahedron of $K$.
proof idea
Unfold the cosine to the cofactor quotient. Let $p,q$ be the opposite Cayley–Menger vertex pair for edge $f$. Invoke the already-proved conformal $C^n$ statements for the off-diagonal cofactor (numerator) and for the dihedral denominator. Nonvanishing of the denominator at the zero potential is immediate from the local nondegeneracy lemma after simplifying the conformal chart at zero. ContDiffAt is closed under division when the denominator is nonzero at the point, which finishes the argument.
why it matters
Parent consumer is tetDihedralAngleUnderConformal_contDiffAt_zero, which lifts this cosine smoothness to dihedral-angle smoothness (arccos) once endpoints stay off $\pm 1$. That angle map is the elementary building block of the nonlinear Regge action on a 3D triangulation. The module’s stated goal is exactly to replace the exact quadratic truncation used by the closed second-order component theorem with genuine smooth nonlinear input at the flat potential. In the broader Recognition geometry stack this is the local analytic gate that lets discrete curvature respond smoothly to conformal vertex potentials, feeding any later continuum or effective-field limit that needs a $C^n$ action near flat space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.