Geometry Cayley Menger N Cm Index Vertex

The index map

The Cayley-Menger matrix is the standard tool for turning a list of pairwise distances into a volume. For a triangle, its determinant gives the area; for a tetrahedron, the volume. The declaration cmIndexVertex is a bookkeeping function that says which row or column of that matrix corresponds to which vertex of the simplex. Index 0 is reserved for the leading row and column, the one filled with ones that makes the determinant work; every other index k+1 points to vertex k. If the index is 0, the function returns nothing; otherwise it returns the matching vertex. That is all it does.

The function matters because the matrix must be built uniformly for any number of dimensions. In three dimensions the tetrahedron has four vertices, so the matrix is 5 by 5: one extra row and column for the leading ones. In n dimensions a simplex has n+1 vertices, so the matrix is (n+2) by (n+2). The index map keeps the correspondence consistent as n changes. The full matrix, called cmMatrixN, uses this map to place a 0 in the top-left corner, a 1 in the leading row and column, and the squared distance between vertices everywhere else. A proved theorem, cmMatrixN_symm, shows that the matrix stays symmetric whenever the distance data is symmetric, which any real set of distances is.

In Recognition Science, this is the first step of a larger project: generalizing the 3D tetrahedral closure to arbitrary dimension. The determinant of the matrix, cmDetN, feeds a formal squared-volume expression, simplexVolumeSqN, that matches the classical formula V_n^2 = (-1)^(n+1) det(CM) / (2^n (n!)^2). The framework's machine-checked library of formal theorems has verified the symmetry property, but it has not yet proved that this determinant actually equals the geometric volume of a simplex. That remains open.

What the declaration does not claim is just as important. It does not assert that any set of distances forms a valid simplex; that requires extra conditions beyond symmetry. It does not prove the volume formula, only defines it. And it says nothing about the physical meaning of the distances, which in the framework would come from the recognition ledger, not from this geometry module.

/-- Convert a Cayley-Menger matrix index to an optional simplex vertex.
Index `0` is the leading Cayley-Menger row/column; index `k+1` represents
simplex vertex `k`. -/
def cmIndexVertex {n : ℕ} (i : Fin (n + 2)) : Option (Fin (n + 1)) :=
  if h : i.val = 0 then none
  else some ⟨i.val - 1, by omega⟩

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

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

What this page does not claim

It does not prove that the determinant equals geometric volume. It does not assert that any symmetric distance data forms a valid simplex. It does not assign physical meaning to the distances.

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: