Geometry Cayley Menger N Cm Det N

The n-simplex volume formula

In classical geometry, the Cayley-Menger determinant answers a practical question: given only the distances between points, can you find the volume of the shape they span? For a triangle, the answer is Heron's formula; for a tetrahedron, a similar expression. The determinant generalizes both. For n points in n-dimensional space, arrange the squared distances in an (n+2) by (n+2) matrix, put 0 on the leading diagonal, 1 in the first row and column, and the squared distances elsewhere. The volume squared is then a fixed multiple of the determinant: V_n^2 = (-1)^(n+1) det(CM) / (2^n (n!)^2). This is the standard formula, known since the nineteenth century.

The Recognition Science library, a machine-checked collection of formal theorems, defines this construction for any dimension n. The declaration cmDetN, a definition, takes a record of squared distances between n+1 vertices and returns the determinant of the full Cayley-Menger matrix. A companion definition, simplexVolumeSqN, applies the classical scaling to produce the squared volume. The library also proves that the matrix is symmetric whenever the distance data is symmetric, a property that holds because distances do not depend on order.

What the declaration does not claim is equally important. It does not prove that the determinant is nonnegative, nor that it corresponds to an actual geometric embedding; those require additional conditions on the distances. It does not derive the formula from the framework's cost function or forcing chain. It is a definitional starting point for the n-dimensional generalization, not a theorem about why three dimensions are special. The volume formula itself is classical; the library's contribution is to formalize it cleanly for arbitrary n, ready for later results.

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

cmDetN does not prove the determinant is nonnegative or that the distances embed in Euclidean space. The volume formula is not derived from the framework's cost function or forcing chain. The declaration does not establish that three dimensions are special.

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: