cmMatrix3
plain-language theorem explainer
Defines the standard 5×5 Cayley–Menger matrix for a tetrahedron from its six squared edge lengths. Anyone proving volume, dihedral cosines, or smoothness of tetrahedral geometry via determinants cites this packing. The body is a pure case table on Fin 5 indices mapping border ones, zero diagonal, and the six edge squares into the classical layout.
Claim. For squared edge lengths $a = (a_0,\ldots,a_5)\in\mathbb{R}^6$ of a tetrahedron (edges $(01),(02),(03),(12),(13),(23)$), the Cayley–Menger matrix $M(a)\in\mathrm{Mat}_{5\times 5}(\mathbb{R})$ is the symmetric matrix with first row/column $(0,1,1,1,1)$, zero diagonal on the remaining $4\times 4$ block, and off-diagonal entries $a_0,\ldots,a_5$ in the classical edge-pair positions.
background
The module sits between the explicit tetrahedral Cayley–Menger polynomial cm3 and the determinant/cofactor layer used for dihedral cosines. Squared edge lengths are packaged as SqEdges := Fin 6 → ℝ, six real numbers for edges $(01),(02),(03),(12),(13),(23)$.
The classical Cayley–Menger matrix for four points in Euclidean space is $5\times 5$: a bordered Gram-type array whose determinant recovers $288 V^2$ (up to sign conventions). Row/column $0$ is the border of ones with a zero corner; the remaining $4\times 4$ block has zeros on the diagonal and squared distances off-diagonal.
This definition materializes that array as a function of the six edge squares so Mathlib's Matrix.det and submatrix minors can be applied directly.
proof idea
Not a proof: a definition by exhaustive pattern match on (i.val, j.val) for i,j : Fin 5. Border cases send the $(0,0)$ corner to $0$ and the rest of row/column $0$ to $1$. The $4\times 4$ distance block places zeros on the diagonal and routes each of the six squared lengths $a,0\ldots a,5$ into both off-diagonal slots (symmetry by construction). Unmatched pairs default to $0$. No lemmas are invoked.
why it matters
This is the matrix substrate for the whole tetrahedron determinant stack. Downstream, cmDet3 is simply Matrix.det of this array; cmDet3_eq_cm3 equates that determinant to the explicit polynomial cm3; cmMinor3 and cofactors delete rows/columns for the dihedral cosine formula. Symmetry (cmMatrix3_symm) and entrywise/ContDiff smoothness (cmMatrix3_entry_contDiff, cmMinor3_contDiff) are proved by finitary case analysis on this table.
In Recognition Science geometry, tetrahedral Cayley–Menger data feed volume and angle identities that sit under discrete spatial structure (forcing chain T8: $D=3$). The definition itself is pure classical geometry; its role is to make the determinant layer machine-checkable and smooth in the edge lengths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.