simplexVolumeSqN
plain-language theorem explainer
Classical squared n-volume of a simplex from its Cayley-Menger determinant: V_n² = (-1)^{n+1} det(CM)/(2^n (n!)^2). Geometry and gravity modules cite it to normalize simplex volumes against squared edge data. The body is a pure definitional encoding of that formula in terms of the n-dimensional CM determinant.
Claim. Given squared-distance data for an $n$-simplex (symmetric, zero diagonal), the formal squared volume is $V_n^2 = (-1)^{n+1}\,\det(\mathrm{CM})/(2^n (n!)^2)$, where $\mathrm{CM}$ is the Cayley-Menger matrix built from those squared distances.
background
The module generalizes Cayley-Menger geometry beyond the 3D tetrahedral case: instead of expanding a fixed-size determinant by hand, it builds the full bordered CM matrix for an arbitrary $n$-simplex and takes Mathlib's determinant.
Squared-distance data is a structure on vertices Fin (n+1): a real matrix of pairwise squared lengths that is symmetric with zero diagonal. The companion cmDetN is simply Matrix.det of the associated CM matrix. The classical identity then recovers squared volume from that determinant with the standard sign and factorial normalization.
Spatial dimension $D=3$ is forced upstream (T8/T9), so the main physical use is the $n=3$ tetrahedron and the $n=4$ causal 4-simplex, but the definition stays parametric in $n$.
proof idea
Definitional, not a proved theorem. The right-hand side is exactly the classical formula: sign factor $(-1)^{n+1}$ times the n-dimensional Cayley-Menger determinant, divided by $2^n (n!)^2$. No lemmas are applied; the body only composes cmDetN with arithmetic on n.
why it matters
Anchors the n-dimensional volume layer that CausalSimplex4D and Wick-action code rely on. Downstream, simplexVolumeSqN_eq_cm4_div proves that for the repo's 4-simplex edge data the expression collapses to cm4 / 9216 (since $2^4(4!)^2=9216$), fixing sign and normalization of the 4D CM determinant against this definition. That identity feeds Euclideanization and positivity criteria (wick_image_euclidean, alphaMin_lt_one) used in the SevenGaps causal-simplex analysis. In the broader RS chain it sits under the forced $D=3$ geometry (T8) while remaining dimension-parametric for the 4-simplex Wick bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.