cmMatrixN
plain-language theorem explainer
Builds the bordered $(n+2)\times(n+2)$ Cayley-Menger matrix from squared edge lengths of an $n$-simplex. Volume formulas, symmetry lemmas, and the 4D causal-simplex gap calculations all cite this matrix. The body is a four-way case split on the bordered index map: corner $0$, border $1$s, interior squared distances.
Claim. Given squared-distance data $D$ on the $n+1$ vertices of an $n$-simplex, form the real $(n+2)\times(n+2)$ matrix $M$ with $M_{00}=0$, $M_{0k}=M_{k0}=1$ for $k\ge 1$, and $M_{ij}=d^2(v_{i-1},v_{j-1})$ for $i,j\ge 1$.
background
This module generalizes the classical Cayley-Menger construction past the fixed 3D tetrahedron: instead of expanding a determinant by hand, it builds a Mathlib matrix for an arbitrary $n$-simplex and takes its determinant later.
Squared-distance data is packaged as SimplexSquaredDistances n: a map $d^2:\mathrm{Fin}(n+1)\times\mathrm{Fin}(n+1)\to\mathbb{R}$ that is symmetric with zero diagonal. Matrix indices live in $\mathrm{Fin}(n+2)$. The helper cmIndexVertex sends index $0$ to "no vertex" (the bordering row/column) and index $k+1$ to simplex vertex $k$.
The classical identity then reads $V_n^2=(-1)^{n+1}\det(M)/(2^n(n!)^2)$, so this matrix is the sole geometric input to every volume and signature computation downstream.
proof idea
Pure definition, no proof obligations. Entry $(i,j)$ is decided by matching the optional vertices of $i$ and $j$: both none gives $0$; exactly one none gives $1$; both some gives the squared distance from the input data. No lemmas are applied.
why it matters
Parent of the n-dimensional Cayley-Menger determinant cmDetN and of the symmetry theorem cmMatrixN_symm. In the gravity stack it is the concrete matrix identified with the two-parameter Euclidean and Lorentzian pentatope matrices for causal types $(4,1)$ and $(3,2)$ (cmMatrixN_euclidean_fourOne, cmMatrixN_lorentzian_fourOne, and the $(3,2)$ twins). Those equalities feed the Seven Gaps causal-simplex analysis. The ambient spatial dimension $D=3$ forced by T8 appears only as the physically preferred specialization $n=3$ (tetrahedron) or $n=4$ (4-simplex); the definition itself stays parametric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.