dihedralDenom3_conformal_contDiffAt_zero
plain-language theorem explainer
At the flat (zero) vertex potential, the Cayley–Menger dihedral denominator of a tetrahedron, pulled back through the conformal squared-edge chart, is C^n for every extended order n. Anyone proving smoothness of the nonlinear Regge action or of squared dihedral cosines near flat space cites this. The proof multiplies two smooth diagonal cofactors and takes a square root, using a local nonvanishing lemma at the flat point.
Claim. Fix a 3D triangulation $K$, a tetrahedron $\tau$, an edge index $f\in\{0,\ldots,5\}$, and an extended differentiability order $n\in\mathbb{N}\cup\{\infty\}$. The map sending a vertex potential $\xi$ to the Cayley–Menger dihedral denominator of the six conformally scaled squared edge lengths of $\tau$ at edge $f$ is $C^n$ as a real function of $\xi$ at the zero potential.
background
This module supplies analytic hypotheses for the full nonlinear Regge action: the conformal edge chart must remain in 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.
The dihedral denominator is $\sqrt{C_{pp}C_{qq}}$, where $C_{rc}$ are Cayley–Menger cofactors of the $5\times 5$ bordered Gram matrix built from squared edge lengths, and $(p,q)$ are the two CM vertex indices opposite the chosen tetrahedral edge. Conformal squared edges are the six local edge lengths of $\tau$ after the conformal ansatz driven by the vertex potential $\xi$.
Upstream, each diagonal cofactor composed with the conformal chart is already $C^n$ at zero potential, and a local lemma asserts the denominator itself is nonzero on the flat configuration (so the square-root branch is smooth there).
proof idea
Unfold the denominator to $\sqrt{C_{pp}C_{qq}}$ with opposite CM indices $(p,q)$. Invoke the already-proved fact that each conformal diagonal cofactor map is $\mathrm{ContDiffAt},n$ at the zero potential; their product is therefore $\mathrm{ContDiffAt},n$ by multiplication of smooth maps.
Nonvanishing of that product at zero potential is reduced to the local lemma that the dihedral denominator is nonzero on the flat tetrahedron: rewrite via the identity that conformal edges at zero potential recover the background squared edges, then contradict the local nonvanishing statement if the product vanished.
Finish by applying the square-root continuity/differentiability lemma for a $C^n$ function that is nonzero at the base point, and simplify the opposite-vertex projections.
why it matters
Smoothness of the nonlinear Regge action at flat space needs every building block of the dihedral cosine to be smooth under the conformal chart. This lemma closes the denominator half of that chain.
Its sole recorded consumer is the companion theorem that the squared dihedral cosine (numerator over this denominator, composed with conformal edges) is $C^n$ at zero potential. That cosine smoothness is the direct analytic input named in the module brief for the finite Regge action near the flat potential.
In the broader Recognition geometry stack this sits under the $D=3$ tetrahedral discretization (forcing landmark T8) and feeds the passage from the exact quadratic truncation of the second-order component theorem to the full nonlinear action, without smuggling nondegeneracy in as an axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.