dihedralCos3Sq_continuousAt_of_den_ne_zero
plain-language theorem explainer
At any squared-edge configuration where the Cayley–Menger dihedral denominator is nonzero, the tetrahedral dihedral cosine (as a function of the six squared edge lengths) is continuous. Analysts of the nonlinear Regge action cite this to justify differentiating or expanding the action near nondegenerate tets. The proof is a short term application of continuous division to a smooth cofactor over a continuous denominator.
Claim. Let $a\in\mathbb{R}^{6}$ be a tuple of squared edge lengths of a tetrahedron and let $e\in\{0,\ldots,5\}$ label an edge. Write $\cos^{2}\theta_{e}(x)$ for the Cayley–Menger dihedral cosine at edge $e$ and $D_{e}(x)$ for its cofactor denominator. If $D_{e}(a)\neq 0$, then $x\mapsto\cos^{2}\theta_{e}(x)$ is continuous at $a$.
background
The 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. Squared edge lengths live in $\mathrm{SqEdges}:=\mathrm{Fin},6\to\mathbb{R}$.
The dihedral cosine is the ratio of a Cayley–Menger cofactor to a geometric mean of diagonal cofactors: $\mathrm{dihedralCos3Sq}(a,e)=C_{pq}(a)/D_{e}(a)$, where $D_{e}(a)=\sqrt{C_{pp}(a)C_{qq}(a)}$ and $(p,q)$ are the vertices opposite edge $e$. Every cofactor $C_{rc}$ is smooth in the edge lengths (cmCofactor3_contDiff). Continuity of the denominator at a fixed configuration is already recorded as dihedralDenom3_continuousAt.
proof idea
Unfold the definition of the dihedral cosine to the quotient of a cofactor by the denominator. Continuity of the numerator at $a$ follows from smoothness of every Cayley–Menger cofactor (cmCofactor3_contDiff at order $0$, evaluated on the opposite-vertex pair for edge $f$). Continuity of the denominator is dihedralDenom3_continuousAt. Continuous division then yields continuity of the quotient at $a$, using the hypothesis that the denominator does not vanish there. The whole argument is a single term-mode application of .div.
why it matters
Smoothness of the nonlinear Regge action at flat configurations needs the dihedral cosines to be continuous (and later differentiable) wherever the tet stays nondegenerate. This lemma is the pointwise continuity engine: the local specialization local_dihedralCos3Sq_continuousAt simply feeds in the triangulation’s squared edges and the already-proved local nonvanishing of the denominator.
Downstream, the gravity analysis gate flat_nondegeneracy_eventually uses the same denominator nonvanishing package to guarantee a neighborhood of the Freudenthal flat tuple on which volumes, edge lengths, and cofactors stay positive. That neighborhood is the analytic chart in which the second-order Regge/TT derivative comparison is legitimate. Within the Recognition geometry stack this is supporting calculus for the closed second-order component theorem’s nonlinear extension, not a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.