Geometry Gram Cayley Menger Gram Cayley Menger Realized

The bridge theorem

The Cayley-Menger determinant is a classical formula that computes the volume of a simplex from the lengths of its edges. For a tetrahedron, the formula takes the six squared edge lengths and returns a number proportional to the squared volume. The Gram matrix approach instead starts from the three edge vectors meeting at a single vertex and uses their pairwise dot products. Both methods are standard in Euclidean geometry, and for a tetrahedron that actually exists in three-dimensional space, they must agree.

The machine-checked library of formal theorems proves this agreement. Its declaration gram_cayley_menger_realized establishes that for every realized tetrahedron, the volume squared computed by the Cayley-Menger determinant equals the volume squared computed from the Gram matrix. The proof works by showing that the squared edge lengths extracted from the Gram matrix match the actual squared distances between the points, and then that the Cayley-Menger polynomial built from those edges equals eight times the determinant of the Gram matrix. The final equality follows by algebra.

Within Recognition Science, this bridge theorem matters because it ties two different ways of encoding the same geometric object. The Cayley-Menger side uses only distances, which are intrinsic to the tetrahedron. The Gram side uses vectors from a chosen basepoint, which depend on a coordinate choice. The theorem says these two encodings carry the same volume information. It is a statement about ordinary Euclidean geometry, not about the recognition ledger or the forcing chain.

The declaration does not claim that every Gram matrix produces a valid tetrahedron. A symmetric 3 by 3 matrix defines edge lengths, but those lengths may fail to correspond to any set of four points in space. The theorem starts with a realized tetrahedron, one that already exists, and proves the two formulas agree on it. It also does not extend to higher dimensions; the proof is specific to the tetrahedral case with three edge vectors. The result is a clean algebraic identity, not a new geometric invariant.

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

/-- For a realized tetrahedron, `cm3` of the extracted squared-edge data
equals `8 * det(Gram)`. -/
theorem cm3_sqEdgeOfPoints_eq_8_det_gram (T : RealizedTet) :
    cm3 (sqEdgeOfPoints T) = 8 * Matrix.det (gram3 T) := by
  rw [sqEdgeOfPoints_eq_sqEdgesFromGram]
  exact cm3_sqEdgesFromGram_eq_8_det (gram3 T) (gram3_symm T)

What this page does not claim

The theorem does not prove that every symmetric Gram matrix corresponds to a realized tetrahedron. The theorem does not extend the equality to simplices beyond the tetrahedral case. The theorem does not connect the Cayley-Menger determinant to the Recognition Science 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/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: