Geometry Gram Cayley Menger

Two paths to one volume

The Cayley-Menger determinant is a classical formula that computes the volume of a simplex, such as a tetrahedron, from the lengths of its edges alone. The Gram determinant is a different classical formula that computes the same volume from the dot products of vectors that emanate from a single vertex. A tetrahedron has six edge lengths and three such vectors, so each formula uses a different slice of the same geometric information. Both are standard tools in metric geometry and distance geometry.

The history runs deep. Arthur Cayley introduced the determinant that bears his name in 1841, and Karl Menger applied it to distance geometry in the 1920s and 1930s, using it to decide when a set of distances can be realized as points in Euclidean space. The Gram determinant is named for Jørgen Pedersen Gram, whose 1879 work on least squares made the matrix of inner products a central object in linear algebra. The two determinants are not obviously equal: one is a polynomial in edge lengths, the other a polynomial in dot products, and they live in different coordinate systems.

The bridge between them is the law of cosines. For three vectors u, v, and w from a common vertex, the squared length of the edge between the tips of u and v is the sum of their squared lengths minus twice their dot product. The module builds squared edge lengths from the Gram matrix this way, then expands the Cayley-Menger polynomial. A direct algebraic expansion, the kind a computer algebra system can verify, shows the tetrahedral Cayley-Menger polynomial equals 8 times the Gram determinant. Dividing by the appropriate constants, the two volume formulas agree exactly.

In Recognition Science, the framework's machine-checked library of formal theorems isolates this bridge as a named theorem, gram_cayley_menger_realized. The library defines a realized tetrahedron as a set of four points in Euclidean space, extracts its squared edge lengths, forms its Gram matrix, and proves the two volume-squared expressions are equal. The proof is not a sketch: it is a formal derivation in the library's logic, with every step checked by the kernel. The theorem holds for every realized tetrahedron, with no hidden regularity assumptions.

The result matters because it connects two ways of describing the same object. Edge lengths are intrinsic: they do not depend on how the tetrahedron sits in space. Dot products are extrinsic: they depend on a chosen basepoint and coordinate axes. The theorem shows that the volume, a quantity that should be intrinsic, can be computed either way, and the two answers always match. This is a consistency check on the framework's geometric foundations, and it gives a concrete tool for translating between metric and linear-algebraic descriptions of a simplex.

The proof is pure algebra once the law of cosines is in hand. The central theorem, cm3_sqEdgesFromGram_eq_8_det, states that the Cayley-Menger polynomial of the squared edges built from a symmetric Gram matrix equals 8 times the determinant of that matrix. The proof unfolds the definitions, expands the 3 by 3 determinant, applies symmetry, and simplifies with the ring tactic. The realized-tetrahedron version follows by showing the edges extracted from points match the edges built from the Gram matrix of the basepoint vectors.

The framework's contribution is not a new formula but a verified guarantee that the classical one is correct. The library states the equivalence in multiple forms, including a determinant-level version, and proves each is equivalent to the polynomial-level statement. For a reader, the practical payoff is a dictionary: any computation that uses edge lengths can be re-expressed using dot products, and the volume is unchanged. This is a small but solid brick in the framework's geometric foundation, one that a curious reader can inspect line by line.

/-- Pure algebra: the tetrahedral Cayley-Menger polynomial generated by a
symmetric Gram matrix equals `8 * det G`. -/
theorem cm3_sqEdgesFromGram_eq_8_det (G : Matrix (Fin 3) (Fin 3) ℝ)
    (hsymm : ∀ i j, G i j = G j i) :
    cm3 (sqEdgesFromGram G) = 8 * Matrix.det G := by
  unfold sqEdgesFromGram cm3
  rw [Matrix.det_fin_three]
  have h10 : G 1 0 = G 0 1 := hsymm 1 0
  have h20 : G 2 0 = G 0 2 := hsymm 2 0
  have h21 : G 2 1 = G 1 2 := hsymm 2 1
  rw [h10, h20, h21]
  ring

/-- The realized tetrahedron satisfies the Gram/Cayley-Menger volume theorem. -/
theorem gram_cayley_menger_realized (T : RealizedTet) :
    volumeSqFromCM T = volumeSqFromGram T := by
  unfold volumeSqFromCM volumeSqFromGram
  rw [cm3_sqEdgeOfPoints_eq_8_det_gram]
  ring

/-- The squared edges extracted from points agree with the squared edges
generated from the Gram matrix of the three basepoint edge vectors. -/
theorem sqEdgeOfPoints_eq_sqEdgesFromGram (T : RealizedTet) :
    sqEdgeOfPoints T = sqEdgesFromGram (gram3 T) := by
  funext e
  fin_cases e
  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
    exact sqDist_eq_baseGram (T.p 0) (T.p 1) (T.p 2)
  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
    exact sqDist_eq_baseGram (T.p 0) (T.p 1) (T.p 3)
  · simp [sqEdgeOfPoints, sqEdgesFromGram, vertexSqDist, edgeVertices3,
      ReggeRigorousFoundation.edgeVertices, gram3, basisEdgeVector, edgeVector]
    exact sqDist_eq_baseGram (T.p 0) (T.p 2) (T.p 3)

/-- The determinant-level and polynomial-level targets are equivalent
because `cmDet3 = cm3`. -/
theorem gram_cayley_menger_det_target_equiv :
    GramCayleyMengerDetTheorem ↔ GramCayleyMengerTheorem := by
  constructor
  · intro h T
    have hT := h T
    rw [cmDet3_eq_cm3] at hT
    exact hT
  · intro h T
    have hT := h T
    rw [cmDet3_eq_cm3]
    exact hT

What this page does not claim

The module does not prove the Cayley-Menger determinant formula itself; it proves the equivalence between the two volume expressions. The theorem applies only to tetrahedra in three-dimensional Euclidean space, not to other simplex dimensions. The proof does not rely on any Recognition Science-specific axiom; it is a theorem of standard linear algebra and geometry.

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/GramCayleyMenger.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: