SimplexSquaredDistances
plain-language theorem explainer
Packages the squared edge lengths of an n-simplex on vertices Fin(n+1) as a symmetric real matrix with zero diagonal. Anyone building Cayley–Menger determinants or n-volume formulas cites this carrier type. It is a pure data structure: two field axioms, no proof obligations beyond the field types.
Claim. For each $n \in \mathbb{N}$, a squared-distance package for an $n$-simplex is a map $d^2 : \{0,\ldots,n\}^2 \to \mathbb{R}$ that is symmetric ($d^2(i,j)=d^2(j,i)$) and vanishes on the diagonal ($d^2(i,i)=0$).
background
The module generalizes the classical Cayley–Menger construction from tetrahedra to arbitrary dimension. Rather than expanding a fixed-size determinant by hand, it builds the full $(n+2)\times(n+2)$ Cayley–Menger matrix from Mathlib matrices and takes its determinant.
An $n$-simplex has $n+1$ vertices, indexed here by Fin (n+1). The only geometric input needed for volume is the table of squared pairwise distances. Symmetry and zero self-distance are the minimal algebraic constraints that make the Cayley–Menger matrix well-defined and symmetric.
Downstream, cmMatrixN fills the bordered matrix (leading 0/1 border, then $-d^2_{ij}$ blocks), cmDetN is its determinant, and simplexVolumeSqN recovers the formal squared volume $V_n^2 = (-1)^{n+1}\det(\mathrm{CM})/(2^n (n!)^2)$.
proof idea
No proof body: this is a structure declaration. The three fields are the squared-distance map, a symmetry proof obligation, and a diagonal-zero proof obligation. Inhabitants are built by supplying a concrete distSq table and discharging the two axioms (typically by rfl or fin_cases on small $n$).
why it matters
This is the input type for the whole dimension-parametric Cayley–Menger stack in the module: cmMatrixN, cmDetN, cmMatrixN_symm, and simplexVolumeSqN all take a SimplexSquaredDistances n. Outside geometry it feeds the 4-simplex (pentatope) edge data in CausalSimplex4D (pentDistances, pentDistSq_edge, wick_image_euclidean), which packages ten squared edges into a 4-simplex for causal/Regge-style analysis. In the Recognition framework this sits under the geometric side of the forcing chain (spatial dimension and discrete simplex structure), supplying the distance carrier once $D=3$ and higher-dimensional causal simplices are in play.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.