cmMatrix3_symm
plain-language theorem explainer
The 5×5 Cayley-Menger matrix of a tetrahedron, built from six squared edge lengths, is symmetric in its indices. Anyone working with the matrix form of tetrahedral volume or dihedral cosines needs this elementary fact. The proof is exhaustive case analysis on Fin 5 followed by definitional equality.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron and any indices $i,j\in\{0,1,2,3,4\}$, the Cayley-Menger matrix satisfies $M(a)_{ij}=M(a)_{ji}$.
background
This module sits in the geometry layer that links the explicit tetrahedral Cayley-Menger polynomial to the genuine $5\times 5$ determinant and its cofactors, the layer required by the dihedral cosine formula. Squared edge lengths are packaged as a map $a:\mathrm{Fin},6\to\mathbb{R}$, ordered as the six edges $(01),(02),(03),(12),(13),(23)$.
The matrix itself is defined entrywise by a match on row and column indices: the $(0,0)$ entry is $0$, the rest of the border is $1$, the diagonal of the $4\times 4$ block is $0$, and the off-diagonal block entries are the corresponding squared lengths. The conventional layout is $$ \begin{pmatrix}0&1&1&1&1\1&0&a_0&a_1&a_2\1&a_0&0&a_3&a_4\1&a_1&a_3&0&a_5\1&a_2&a_4&a_5&0\end{pmatrix}. $$ Symmetry of this array is immediate from the definition but must be recorded before determinant and cofactor identities are used.
proof idea
Both indices range over a five-element type. The proof runs fin_cases on the first index, then on the second, producing twenty-five goals. Each goal is definitional equality of two match-expressions that evaluate to the same real (border ones, zeros on the diagonal block, or the same squared length $a_k$), discharged by rfl. No algebraic lemmas are required; the matrix constructor is already written symmetrically.
why it matters
Symmetry is the first structural property needed before one equates Mathlib's determinant of this matrix to the explicit polynomial cm3, and before cofactors feed the dihedral cosine formula. The module header states that this determinant/cofactor layer is exactly what the dihedral cosine pipeline consumes. In the broader Recognition geometry stack the tetrahedron is the 3-simplex in the forced spatial dimension $D=3$ (forcing step T8), so volume and angle identities built on Cayley-Menger sit on the same geometric spine. Downstream use count is currently empty in the graph, but sibling results (cmDet3_eq_cm3, cofactor continuity, regular and right-angle unit evaluations) all presuppose a well-behaved symmetric matrix.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.