Geometry Cayley Menger N Simplex Squared Distances

The Cayley-Menger determinant in any dimension

The Cayley-Menger determinant is a classical formula that answers a surprising question: given only the lengths of the edges of a triangle, tetrahedron, or higher-dimensional simplex, what is its volume? For a triangle with sides a, b, c, the determinant of a 3 by 3 matrix built from those squared lengths yields the area via Heron's formula. For a tetrahedron, the same construction with a 4 by 4 matrix gives the volume. The formula generalizes to any dimension n: an n-simplex (a triangle in 2D, a tetrahedron in 3D, a pentachoron in 4D) has n+1 vertices, and its squared volume is proportional to the determinant of an (n+2) by (n+2) matrix whose entries are squared distances between vertices, with a border of ones and a zero corner.

Arthur Cayley first studied the determinant in 1841, and Karl Menger used it in 1928 to characterize when a set of distances can be realized as a Euclidean simplex. The formula's power is that it needs only pairwise distances, not coordinates. For an n-simplex, the squared volume V_n^2 equals (-1)^(n+1) times the determinant, divided by 2^n times (n!) squared. The sign factor ensures the result is positive for a genuine simplex. When the determinant is zero, the points are degenerate, lying in a lower-dimensional flat; when it is negative, the distances cannot come from any Euclidean simplex at all.

The Recognition Science framework's machine-checked library of formal theorems has now formalized this construction for arbitrary n. Its declaration SimplexSquaredDistances defines the raw data: a function assigning a real number to each pair of vertices, with two axioms: symmetry, so the distance from i to j equals the distance from j to i, and zero on the diagonal, so each vertex is distance zero from itself. From that data, the library builds the full (n+2) by (n+2) matrix, computes its determinant, and defines the formal squared-volume expression exactly as the classical formula states. It also proves that the matrix is symmetric whenever the distance data is symmetric, a small but necessary consistency check.

What this establishes, in plain terms, is a rigorous definitional foundation: the classical Cayley-Menger formula now exists as a formal object for every dimension, not just 2 or 3. What it does not claim is that any particular set of distances actually comes from a real simplex. The formal definitions work with arbitrary real numbers; they do not check whether a given distance matrix is realizable. Realizability is a separate question, one that Menger's theorem addresses, and it is not part of this declaration. The library also does not prove that the formula gives the true geometric volume of an embedded simplex; that would require a separate geometric construction. The value here is the foundation: a clean, machine-checked starting point for future theorems about volumes, degeneracy, and the geometry of higher-dimensional simplices.

/-- Squared-distance data for an `n`-simplex with vertices `Fin (n+1)`. -/
structure SimplexSquaredDistances (n : ℕ) where
  distSq : Fin (n + 1) → Fin (n + 1) → ℝ
  symm : ∀ i j, distSq i j = distSq j i
  diag_zero : ∀ i, distSq i i = 0

/-- The full `(n+2) × (n+2)` Cayley-Menger matrix. -/
def cmMatrixN {n : ℕ} (D : SimplexSquaredDistances n) :
    Matrix (Fin (n + 2)) (Fin (n + 2)) ℝ :=
  fun i j =>
    match cmIndexVertex i, cmIndexVertex j with
    | none, none => 0
    | none, some _ => 1
    | some _, none => 1
    | some vi, some vj => D.distSq vi vj

/-- The formal squared-volume expression:

`V_n^2 = (-1)^(n+1) det(CM) / (2^n (n!)^2)`.
-/
def simplexVolumeSqN {n : ℕ} (D : SimplexSquaredDistances n) : ℝ :=
  ((-1 : ℝ) ^ (n + 1) * cmDetN D) /
    ((2 : ℝ) ^ n * ((Nat.factorial n : ℕ) : ℝ) ^ 2)

/-- The Cayley-Menger matrix is symmetric whenever the squared-distance
data is symmetric. -/
theorem cmMatrixN_symm {n : ℕ} (D : SimplexSquaredDistances n)
    (i j : Fin (n + 2)) :
    cmMatrixN D i j = cmMatrixN D j i := by
  unfold cmMatrixN
  cases cmIndexVertex i <;> cases cmIndexVertex j <;> simp
  exact D.symm _ _

What this page does not claim

The declaration does not prove that any given distance matrix is realizable as a Euclidean simplex. The declaration does not prove that the formal expression equals the geometric volume of an embedded simplex.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/CayleyMengerN.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: