dihedralDenom3_continuousAt
plain-language theorem explainer
At every squared-edge configuration of a tetrahedron, the Cayley-Menger dihedral denominator (square root of the product of the two opposite cofactors) is continuous in the six edge-square coordinates. Anyone proving continuity of dihedral cosines or of the nonlinear Regge action near flat configurations cites this. The proof is a short term argument: ContDiff of each cofactor yields ContinuousAt, then product and square-root preserve continuity.
Claim. For every squared-edge assignment $a:\mathrm{Fin}\,6\to\mathbb{R}$ and every edge index $f\in\mathrm{Fin}\,6$, the map $x\mapsto \sqrt{C_{p,p}(x)\,C_{q,q}(x)}$ is continuous at $a$, where $(p,q)$ are the two Cayley-Menger vertex indices opposite edge $f$ and $C_{r,c}$ is the corresponding Cayley-Menger cofactor.
background
The module collects analytic hypotheses needed 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. These are recorded as named configuration facts rather than axioms.
Squared edge lengths live in $\mathrm{SqEdges}:=\mathrm{Fin},6\to\mathbb{R}$. For each edge $e$, oppositeCMVertices returns the pair of Cayley-Menger indices opposite that edge. The dihedral denominator is then $\sqrt{C_{p,p}(a),C_{q,q}(a)}$, with $C_{r,c}$ the signed Cayley-Menger cofactor (minor times sign). Upstream, every cofactor is smooth: cmCofactor3_contDiff gives $\mathrm{ContDiff},\mathbb{R},n$ in the six edge-squares for any $n$, hence ordinary continuity.
proof idea
Unfold the denominator definition and name the opposite vertex pair $(p,q)$ for the given edge. Apply cmCofactor3_contDiff at order $0$ to each diagonal cofactor $C_{p,p}$ and $C_{q,q}$; ContDiff implies Continuous, hence ContinuousAt the base point $a$. The product of two ContinuousAt maps is ContinuousAt, and Real.sqrt is continuous on $\mathbb{R}$, so the composite $\sqrt{C_{p,p},C_{q,q}}$ is ContinuousAt $a$. Finish by simpa to match the unfolded definition.
why it matters
This is the first continuity brick for dihedral data in the Regge smoothness stack. Downstream, dihedralCos3Sq_continuousAt_of_den_ne_zero uses it (together with cofactor continuity and a nonzero-denominator hypothesis) to get ContinuousAt for the squared dihedral cosine. That feeds local continuity of dihedral cosines on the nondegenerate cone, which the module needs so the nonlinear Regge action is smooth at the flat potential rather than only at the exact quadratic truncation of the closed second-order component theorem.
In the broader Recognition geometry layer this supports analytic control of discrete curvature (Regge deficit angles) near flat configurations, a prerequisite for matching continuum limits and for any later claim that the action is ContDiff in edge lengths. It does not itself touch the forcing chain (T0-T8) or RCL; it is pure tetrahedral Cayley-Menger analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.