cmDet3_rightAngle_unit
plain-language theorem explainer
The Cayley-Menger determinant of the right-angle unit tetrahedron (three orthogonal unit edges from one vertex) equals 8. Volume-formula and dihedral-cosine checks cite this as the classical V = 1/6 sanity case. Proof is a two-step rewrite: matrix det equals the explicit polynomial, then the known polynomial evaluation.
Claim. Let $a$ be the six squared edge lengths of the right-angle unit tetrahedron (three mutually orthogonal unit edges from one vertex, with the three face diagonals and space diagonal fixed by Pythagoras). Then the $5\times 5$ Cayley-Menger determinant of $a$ equals $8$.
background
This module links the explicit tetrahedral Cayley-Menger polynomial cm3 to the actual $5\times 5$ matrix determinant. The matrix convention borders a $4\times 4$ block of squared edge lengths $a_0,\ldots,a_5$ (edges $(01),(02),(03),(12),(13),(23)$) by a first row/column of ones and a zero corner, exactly the classical Cayley-Menger layout used for tetrahedron volume.
The right-angle unit edge data places three orthogonal unit legs at one vertex: squared lengths $1,1,1$ on those legs, with the remaining three edges determined by the Euclidean embedding. Classically $V=1/6$, and the identity $288 V^2$ recovers the constant $8$.
Upstream, the matrix determinant is defined via Mathlib's Matrix.det, and a prior theorem equates that determinant to the expanded polynomial cm3 for every squared-edge 6-tuple. A sibling polynomial theorem already evaluates cm3 on this edge data to $8$.
proof idea
One-line rewrite wrapper. First apply the identity that the Mathlib determinant of the Cayley-Menger matrix equals the explicit polynomial cm3 on any squared-edge input. Then apply the already-proved polynomial evaluation that cm3 on the right-angle unit edge data is $8$. No matrix expansion or arithmetic is redone at this layer.
why it matters
Closes the matrix-side sanity check for the right-angle unit tetrahedron, matching the classical volume identity $288 V^2 = 8$ when $V=1/6$. The module exists as the determinant/cofactor layer required by the dihedral cosine formula; this theorem confirms that the matrix presentation agrees with the polynomial on the standard orthogonal test case, parallel to the regular-unit check in the same file.
No downstream consumers are wired yet in the graph. In the broader Recognition geometry stack it is a low-level consistency pin for tetrahedron volume and hinge data (Regge-style edge assignments), not a forcing-chain (T0–T8) step. It does not touch $\varphi$, the eight-tick octave, or the $\alpha$ band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.