Geometry Cayley Menger N Cm Matrix N

The n-dimensional Cayley-Menger matrix

The Cayley-Menger matrix is a classical tool in geometry: given the pairwise squared distances between n+1 points, it packages them into a matrix whose determinant tells you the volume of the simplex those points span. In three dimensions, the tetrahedral version is well known. The Recognition Science declaration cmMatrixN extends this to arbitrary dimension n, building the full (n+2) by (n+2) matrix for an n-simplex with vertices indexed by Fin (n+1).

The construction is clear once you see the pattern. The matrix has one extra row and column, the leading row and column, which encode the constant 1 entries that anchor the volume formula. For two actual vertices, the entry is their squared distance; for the leading index paired with a vertex, the entry is 1; and the leading diagonal entry is 0. The declaration cmMatrixN defines exactly this matrix, and a companion definition cmDetN takes its determinant. From that determinant, the formal squared volume follows: V_n^2 = (-1)^(n+1) det(CM) / (2^n (n!)^2).

What does this establish in plain terms? It gives a uniform, machine-checked definition that works for any n, not just the familiar 2D triangle or 3D tetrahedron. It also proves a basic structural fact: the matrix is symmetric whenever the squared-distance data is symmetric, which is always true for real distances. That symmetry is a theorem, not an assumption, and it follows directly from the definition.

In Recognition Science, this declaration is a stepping stone: it starts the n-dimensional generalization after the 3D tetrahedral closure. The framework does not claim that any particular n is forced here. The declaration merely sets up the algebraic object; it does not derive the three spatial dimensions, nor does it connect the matrix to the framework's forcing chain. It is a definitional foundation, not a physical result.

The practical payoff is that any future work on higher-dimensional simplices, whether in geometry or in the framework's own development, can rely on this single matrix definition and its determinant. It is a clean, general tool, ready for use.

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

This declaration does not prove that three spatial dimensions are forced. It does not derive the fine-structure constant or any physical constant. It does not connect the Cayley-Menger matrix to the framework's cost function or recognition ledger.

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: