local_dihedralCos3Sq_continuousAt
plain-language theorem explainer
At the squared edge lengths of any tetrahedron in a 3D triangulation, the Cayley–Menger squared dihedral cosine (as a map on six squared edges) is continuous. Anyone proving smoothness of the nonlinear Regge action near the flat configuration cites this. The proof is a one-line application of the denominator-nonzero continuity lemma plus local non-vanishing of the dihedral denominator on that tetrahedron.
Claim. Let $K$ be a 3D triangulation, $\tau$ any tetrahedron of $K$, and $f\in\{0,\ldots,5\}$ an edge index. The map sending six squared edge lengths $x$ to the squared dihedral cosine of edge $f$ (Cayley–Menger cofactor over dihedral denominator) is continuous at the squared edge lengths of $\tau$.
background
This module supplies analytic inputs for the full nonlinear Regge action: the conformal edge chart must stay in the nondegenerate tetrahedral cone, arccos arguments must avoid $\pm 1$, and the finite Regge action must be smooth at the flat potential. Those requirements are recorded as named configuration facts rather than axioms.
Squared edge data live in $\mathrm{SqEdges}:=\mathrm{Fin},6\to\mathbb{R}$. The squared dihedral cosine $\mathrm{dihedralCos3Sq}(a,e)$ is the ratio of a Cayley–Menger $3\times 3$ cofactor to the dihedral denominator $\mathrm{dihedralDenom3}(a,e)$. Continuity of that ratio at a point $a$ is already known whenever the denominator is nonzero. Separately, on any tetrahedron of a triangulation $K$, that denominator is nonzero at the tetrahedron's own squared edges (via the polynomial form of the denominator and a strict-positivity lemma on the local chart).
proof idea
One-line wrapper. Instantiate the general continuity lemma (squared dihedral cosine continuous at $a$ whenever $\mathrm{dihedralDenom3}(a,f)\neq 0$) at $a=((K.\mathrm{tet},\tau).\mathrm{sqEdge})$, and discharge the denominator hypothesis by the local non-vanishing theorem for triangulation tetrahedra. No further unfolding or continuity algebra is done here.
why it matters
Parent use is continuity of the squared dihedral cosine along the conformal edge chart at the zero (flat) vertex potential: that argument takes this base continuity at the tetrahedron's squared edges and composes with continuity of the conformal chart map. Together these steps feed the module's program of making the nonlinear Regge action smooth at the flat potential, rather than working only with the exact quadratic truncation of the closed second-order component theorem. In the geometry stack this is a local analytic gate: without continuous dihedral cosines at physical edge data, arccos-based deficit angles and the Regge action cannot be treated as continuous (let alone smooth) inputs near flat space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.