IndisputableMonolith.Geometry.CayleyMengerN
Dimension-parametric Cayley–Menger data for an n-simplex on vertices Fin(n+1): squared edge lengths, the bordered CM matrix, its determinant, and the squared volume formula. Geometers and the Schläfli/causal-simplex lanes cite it as the shared distance-to-volume interface. The module is definitional scaffolding over Mathlib matrices and determinants, with a symmetry lemma for the CM matrix.
claimFor an $n$-simplex with vertices indexed by $\mathrm{Fin}(n+1)$, package squared pairwise distances $d_{ij}^2$, form the bordered Cayley–Menger matrix $CM_n$, and define the squared volume via $\mathrm{Vol}^2 \propto |\det CM_n|$ (up to the standard combinatorial prefactor in $n$).
background
The classical Cayley–Menger determinant recovers the squared volume of a Euclidean simplex from its edge-length data alone. In the bordered form, one builds an $(n+2)\times(n+2)$ symmetric matrix whose interior block holds squared distances $d(v_i,v_j)^2$, with a bordering row and column of ones (and a zero corner). The determinant of that matrix is proportional to $(-1)^{n+1} 2^n (n!)^2$ times the squared $n$-volume.
This module fixes the finite-index convention: vertices live in $\mathrm{Fin}(n+1)$, squared distances are a map on pairs, and the CM matrix, its determinant, and the squared-volume expression are named objects rather than ad-hoc constructions. Imports are only Mathlib reals, matrices, and determinants; no Recognition-specific physics enters here.
Downstream geometry (Schläfli identities) and the 4D causal-simplex / CDT lane both need a uniform n-parametric volume-from-distances hook; this file supplies that hook.
proof idea
This is a definition module, not a theorem chain. It introduces squared-distance data on Fin(n+1), index conventions for the bordered matrix, the Cayley–Menger matrix and determinant, and the squared-volume abbreviation. The only nontrivial lemma-level content indicated among siblings is symmetry of the CM matrix (immediate from symmetry of squared distances). No deep algebraic identity is proved here; volume laws and Schläfli relations live downstream.
why it matters in Recognition Science
SchlaefliN imports this module to state the n-dimensional Schläfli identity in finite-index form, with the 3D tetrahedral case intended as the n=3 instance. CausalSimplex4D (QG Seven-Gaps, Lorentzian sector, Phase 3a) imports it for CDT-style 4-simplex classes and the kinematical Wick rotation in D=4, lifting the 3D causal-simplex machinery. Without a shared CM interface, those lanes would each rebuild distance-to-volume bookkeeping. In the broader Recognition geometry stack this is pure Euclidean scaffolding: it does not itself force D=3 (T8) or the eight-tick structure, but it is the volume primitive those geometric arguments sit on.
scope and limits
- Does not prove the classical Cayley–Menger volume identity from first principles.
- Does not treat Lorentzian or causal signature; only Euclidean squared-distance data.
- Does not specialize to n=3 or n=4; those instances live in importers.
- Does not encode Schläfli angle relations or deficit angles.
- Does not connect to RS forcing chain landmarks (phi, eight-tick, T8).