cmDet3_contDiff
plain-language theorem explainer
The 5×5 Cayley-Menger determinant of a tetrahedron, as a real function of the six squared edge lengths, is of class C^n for every extended natural order n (including C^∞). Cite this when transferring smoothness of tetrahedral volume or dihedral data from the explicit polynomial form to the matrix-determinant form. The argument is a short transfer: pointwise equality of the two maps, then rewrite onto the known ContDiff result for the polynomial.
Claim. For every extended natural number $n\in\mathbb{N}\cup\{\infty\}$, the map from six squared edge lengths to the real $5\times 5$ Cayley-Menger determinant is of class $C^n$ over $\mathbb{R}$.
background
This module sits in the tetrahedral geometry layer: it ties the explicit Cayley-Menger polynomial in six squared edge lengths to Mathlib's determinant of the standard $5\times 5$ bordered Cayley-Menger matrix. The matrix convention places a zero border row/column of ones, then the six squared lengths $(01),(02),(03),(12),(13),(23)$ in the usual off-diagonal slots. That determinant/cofactor package is the algebraic input to the dihedral cosine formula.
Write $\mathrm{cmDet3}$ for the determinant of that matrix and $\mathrm{cm3}$ for the expanded multilinear polynomial in the six squared lengths. An upstream identity proves they agree pointwise on all real six-tuples. Separately, $\mathrm{cm3}$ is already known to be $C^n$ for every $n$, built from the ring operations and coordinate projections via the standard ContDiff calculus rules.
proof idea
Short transfer proof. First obtain function equality $\mathrm{cmDet3}=\mathrm{cm3}$ by funext and the pointwise identity that Mathlib's matrix determinant equals the explicit polynomial. Rewrite the goal along that equality, then apply the existing ContDiff theorem for the polynomial at the same order $n$. No fresh smoothness estimates are computed on the matrix side.
why it matters
Smooth dependence of the Cayley-Menger determinant on edge data is the analytic prerequisite for treating tetrahedral volume, Gram determinants, and dihedral cosines as smooth (or $C^\infty$) functions of metric input. The module doc states this determinant/cofactor layer is exactly what the dihedral cosine formula needs. In the broader Recognition geometry stack that feeds continuum and Regge-style limits, one wants to differentiate or expand these quantities without leaving the smooth category. No downstream consumers are wired in the current graph, so the lemma is presently a leaf that closes the smoothness obligation for the matrix form once the polynomial form is smooth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.