cmDetN
plain-language theorem explainer
The n-dimensional Cayley-Menger determinant of an n-simplex: the determinant of the bordered squared-distance matrix. Anyone computing simplex volume from edge lengths, or specializing to 4-simplex causal volumes, cites this as the raw det input. The body is a one-line wrapper applying Mathlib matrix determinant to the parametric Cayley-Menger matrix.
Claim. For $n \in \mathbb{N}$ and squared-distance data $D$ on the $n+1$ vertices of an $n$-simplex, the Cayley-Menger determinant is $\det(\mathrm{CM}_n(D)) \in \mathbb{R}$, where $\mathrm{CM}_n(D)$ is the $(n+2)\times(n+2)$ bordered matrix built from $D$.
background
This module begins the n-dimensional generalization after 3D tetrahedral closure: rather than expanding a fixed-size determinant as a polynomial, it defines the full Cayley-Menger matrix for an arbitrary n-simplex via Mathlib matrices and determinants.
Squared-distance data for an n-simplex is a symmetric map on vertex pairs in $\mathrm{Fin}(n+1)$ with zero diagonal. The Cayley-Menger matrix is the $(n+2)\times(n+2)$ matrix whose leading index is the classical 0/1 border and whose interior block holds those squared edge lengths. Framework constants fix spatial dimension $D=3$ (T8), but this definition stays parametric in $n$.
proof idea
One-line definitional wrapper: evaluate Mathlib Matrix.det on cmMatrixN D, the already-built $(n+2)\times(n+2)$ Cayley-Menger matrix of the given squared-distance data. No algebraic expansion or case split.
why it matters
Feeds the formal squared-volume formula $V_n^2 = (-1)^{n+1}\det(\mathrm{CM})/(2^n (n!)^2)$ in the sibling volume definition. Downstream, the SevenGaps causal 4-simplex layer sets cm4 to the sign-normalized $n=4$ case and proves Euclidean and Lorentzian evaluations for AJL types (4,1) and (3,2): e.g. Euclidean (4,1) gives $(8\alpha-3)a^8$, matching $9216 V^2$ against the AJL volume formula. Those theorems unfold through this determinant, linking discrete 4-volume in the gravity stack to the parametric geometry layer after tetrahedral closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.