Geometry Cayley Menger N

The n-dimensional volume formula

The Cayley-Menger determinant is a classical tool from distance geometry. It answers a question that sounds impossible: how do you find the volume of a triangle, tetrahedron, or higher-dimensional simplex when all you know is the lengths of its edges? The answer is a single determinant built from those squared distances. For a triangle with side lengths a, b, c, the determinant yields the area; for a tetrahedron, it yields the volume. The formula generalizes to any number of dimensions.

The classical formula is V_n² = (-1)^(n+1) det(CM) / (2^n (n!)²), where CM is the Cayley-Menger matrix. The matrix has size (n+2) × (n+2) for an n-dimensional simplex. Its first row and column are mostly 1s with a 0 in the corner, and the remaining block holds the squared distances between vertices. The determinant of this matrix, with the sign and factorial factors, gives the squared volume. This is the standard result that lets geometers compute volumes from distances alone, without ever placing coordinates.

In Recognition Science, this classical tool gets a formal treatment. The framework's machine-checked library of formal theorems defines the Cayley-Menger matrix for an arbitrary n-simplex, not just the familiar 2D and 3D cases. The module starts with a structure called SimplexSquaredDistances, a discrete record of the squared distances between every pair of vertices. It then builds the full (n+2) × (n+2) matrix and defines the determinant and the volume formula exactly as the classical version states them.

The module also proves that the Cayley-Menger matrix is symmetric whenever the squared-distance data is symmetric. This is a small but necessary lemma: it confirms that the matrix behaves as expected, since distances are inherently symmetric. The proof is a direct case analysis on the matrix entries, using the symmetry of the distance data. It is a formal verification of a property that mathematicians have long taken for granted.

What this establishes in plain language is that the classical volume formula is not just a heuristic but a precisely defined object that can be handled rigorously in any dimension. The framework models the n-dimensional case as a definitional choice, not as a derived theorem. The symmetry property is proved, but the volume formula itself is defined, not derived from deeper principles. This is a foundation for future work, not a finished result about the physical world.

/-- 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 n-dimensional Cayley-Menger determinant. -/
def cmDetN {n : ℕ} (D : SimplexSquaredDistances n) : ℝ :=
  Matrix.det (cmMatrixN D)

/-- 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

This module does not prove that the volume formula gives the actual geometric volume of a simplex. This module does not derive the Cayley-Menger determinant from the framework's cost function or forcing chain.

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: