cmMatrixN_symm
plain-language theorem explainer
The Cayley-Menger matrix of an n-simplex is a symmetric real matrix whenever the input squared distances are symmetric. Anyone proving volume identities, determinant formulae, or positive-semidefiniteness for the n-dimensional Cayley-Menger construction would cite this. The proof unfolds the matrix definition, case-splits on the border-versus-vertex index map, and invokes distance symmetry on the interior block.
Claim. Fix $n\in\mathbb{N}$ and a squared-distance assignment $d$ on the $n+1$ vertices of an $n$-simplex with $d(i,j)=d(j,i)$ for all vertices and $d(i,i)=0$. Let $M$ be the associated $(n+2)\times(n+2)$ Cayley-Menger matrix (leading border row/column of $0$ and $1$s, interior block $-d(u,v)^2$). Then $M_{ij}=M_{ji}$ for every pair of matrix indices $i,j$.
background
This module begins the dimension-parametric Cayley-Menger construction after the 3D tetrahedral case: rather than expanding a fixed-size determinant by hand, it defines the full matrix for an arbitrary $n$-simplex via Mathlib matrices and determinants.
Squared-distance data for an $n$-simplex is a map $d$ on $\mathrm{Fin}(n+1)\times\mathrm{Fin}(n+1)$ required to be symmetric with zero diagonal. Matrix indices live in $\mathrm{Fin}(n+2)$; the helper that sends index $0$ to the leading Cayley-Menger border and index $k+1$ to simplex vertex $k$ decides each entry. The matrix itself is $0$ at the $(0,0)$ corner, $1$ along the rest of the border, and $-d(u,v)$ on the interior block.
Several upstream modules fix a constant spatial dimension $D=3$ (T8/T9 forcing), but the present lemma is parametric in $n$ and does not specialize that constant.
proof idea
Unfold the matrix definition so each entry is a match on the border-versus-vertex index map for $i$ and for $j$. Case-split on both optional vertices (four combinations: border/border, border/vertex, vertex/border, vertex/vertex). In the three border cases, simp closes the equalities from the literal $0$ and $1$ entries. In the interior case, apply the symmetry field of the squared-distance structure to the two vertices.
why it matters
Symmetry is the first structural property needed before determinants, principal minors, or the squared-volume formula can be treated as well-defined geometric invariants rather than ordered-array artefacts. The module's goal is the $n$-simplex volume squared extracted from $\det M$; without $M=M^\top$, sign and factor conventions become ambiguous under index swaps.
In the Recognition Science geometry stack this sits after the 3D tetrahedral closure and prepares the same Cayley-Menger route in variable dimension. Framework landmark T8 forces physical space to $D=3$, so the physically used instance is the $n=3$ specialization, but the lemma is proved uniformly so the 3D case is not a special snowflake. No downstream theorems yet depend on it in the graph; it is infrastructure for cmDetN / simplexVolumeSqN and later rigidity or embedding arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.