Geometry Cayley Menger N Simplex Volume Sq N

The n-simplex volume formula

The Cayley-Menger determinant is the classical tool that answers a simple question: given all the pairwise distances between the vertices of a triangle, tetrahedron, or their higher-dimensional cousins, what is the volume? For a triangle with side lengths a, b, c, the determinant of a certain matrix built from those lengths yields the area squared. For a tetrahedron, the same construction yields the volume squared. The pattern continues for any n-simplex, the generalization of a triangle (n = 2) or tetrahedron (n = 3) to n dimensions.

The formula itself is compact. For an n-simplex with vertices labeled 0 through n, form the (n+2) by (n+2) matrix whose top row and left column are all 1 except for a 0 in the corner, and whose lower-right block holds the squared distances between vertices. Then the squared volume is

V_n² = (−1)ⁿ⁺¹ det(CM) / (2ⁿ (n!)²).

The sign factor and denominator adjust the determinant so that the result is exactly the square of the usual Euclidean volume. This formula was known in essence to Arthur Cayley in 1841 and extended by Karl Menger in the 1920s, who used it to characterize when a set of distances can come from points in Euclidean space.

In Recognition Science, the framework's machine-checked library of formal theorems defines this construction for arbitrary n as a ledger, a discrete record of events, here the squared distances between every pair of vertices. The definition simplexVolumeSqN states the formula above as a formal expression. The library proves that the Cayley-Menger matrix is symmetric whenever the distance data is symmetric, a property that holds automatically for real distances. What the declaration does not do is prove that this expression equals the actual geometric volume of any embedded simplex; that would require a separate theorem connecting the algebraic determinant to a metric notion of volume. The declaration also does not assert that the distances come from points in Euclidean space; Menger's conditions for that are a different result.

What this gives a reader is a single, uniform formula that works in every dimension, from a line segment (n = 1, where it returns the squared length) to a 10-simplex in ten dimensions. The value is not a new geometric discovery but a clean formal statement that the classical formula extends without case splits, a foundation on which later theorems about simplex volume can be built.

/-- 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 formula is not proved to equal the geometric volume of an embedded simplex. The definition does not assert that the given distances arise from points in Euclidean space. No claim is made about the sign or positivity of the determinant for arbitrary distance data.

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: