cmDet3_scaling
plain-language theorem explainer
The 5x5 Cayley-Menger determinant of a tetrahedron scales by s cubed when every squared edge length is multiplied by the same real factor s. Volume and dihedral-angle arguments under uniform similarity cite this homogeneity. The proof is a three-step rewrite: equate the matrix determinant to the explicit polynomial, apply the polynomial's cubic scaling law, and equate back.
Claim. Let $a$ assign six real squared edge lengths to a tetrahedron, and let $s\in\mathbb{R}$. Writing $D(a)$ for the determinant of the associated $5\times 5$ Cayley-Menger matrix, one has $D(s\cdot a)=s^3\,D(a)$.
background
This module sits in the determinant/cofactor layer that links the explicit tetrahedral Cayley-Menger polynomial to the actual $5\times 5$ matrix determinant used by the dihedral cosine formula. Squared edge lengths are packaged as a map $a:\mathrm{Fin},6\to\mathbb{R}$ (edges $(01),(02),(03),(12),(13),(23)$). The matrix convention borders a $4\times 4$ Gram-like block of those squared lengths by a row and column of ones, with zeros on the diagonal of the length block.
The determinant $D(a)$ is Mathlib's matrix determinant of that bordered matrix. An upstream identity proves $D(a)$ equals the explicit degree-three polynomial $\mathrm{cm}_3(a)$ in the six squared lengths. Separately, that polynomial obeys the classical scaling law: if every squared length is multiplied by $s$, then $\mathrm{cm}_3$ multiplies by $s^3$ (consistent with $V\mapsto s^{3/2}V$, hence $V^2\mapsto s^3 V^2$).
proof idea
One-line rewrite proof. Replace the matrix determinant by the explicit polynomial via the equality theorem, invoke the polynomial scaling identity (itself a direct ring expansion of $\mathrm{cm}_3$), then replace the polynomial by the matrix determinant again. No expansion of the $5\times 5$ determinant is needed at this layer.
why it matters
Homogeneity of the Cayley-Menger determinant under edge scaling is the matrix-side counterpart of the classical volume scaling $V\propto L^3$. The module's stated purpose is to supply the determinant/cofactor layer required by the dihedral cosine formula; cubic scaling is the basic covariance check that formula must inherit. No downstream consumers are wired yet in the graph, so the result presently closes the scaling section of the matrix layer rather than feeding a named parent theorem. Within Recognition Science geometry it keeps the tetrahedral volume proxy consistent under the same similarity moves that act on the phi-ladder and eight-tick discrete structures, without yet touching the forcing chain T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.