Geometry Tetrahedron Realization Gram Cayley Menger Volume Theorem

The volume identity

A tetrahedron is the simplest solid shape in three dimensions: four corner points, six edges, and four triangular faces. Its volume can be computed from the coordinates of its corners, but there is also a classical formula, the Cayley-Menger determinant, that uses only the six squared edge lengths. The declaration GramCayleyMengerVolumeTheorem states that for any tetrahedron realized by four points in Euclidean 3-space, these two volume formulas give the same answer.

The theorem is a definition in the framework's machine-checked library of formal theorems, not a separate proof. It asserts a proposition: for every realized tetrahedron, the volume squared from the Cayley-Menger formula equals the volume squared from the Gram matrix of the three edge vectors meeting at one vertex. The Gram matrix is the table of dot products among those three vectors; its determinant divided by 36 gives the squared volume. The Cayley-Menger formula instead takes the six squared edge lengths and divides by 288. The declaration packages the equality as a target for later proof.

This identity is not new mathematics. It is a standard result in Euclidean geometry, and the declaration formalizes it inside the framework's library. The library has already proved that the Gram matrix is symmetric and that squared edge lengths from points are nonnegative, and it has proved the defining identity that the Gram determinant equals 36 times the Gram-based squared volume. What the declaration adds is the statement that the two volume routes agree for every nondegenerate tetrahedron, where nondegenerate means the four points are affinely independent, so they do not lie in a plane.

In Recognition Science, this theorem matters because the framework derives physical structure from a ledger of recognition events, and geometry enters through such exact classical identities. The declaration is a bridge: it connects the abstract six squared-edge coordinates used in the Cayley-Menger layer to actual points in Euclidean 3-space. It does not itself prove that the bridge is sound; it names the claim that the library will later establish.

What the declaration does not claim is broader than what it asserts. It does not claim that every six numbers form a valid tetrahedron; the Cayley-Menger determinant must be positive and satisfy triangle inequalities for that. It does not claim any theorem about the sign of the volume, since the statement uses squared volume. And it does not claim that the identity holds for degenerate tetrahedra, where the four points are coplanar; the nondegenerate hypothesis is explicit in the definition of a realized tetrahedron.

/-- The theorem target connecting the Euclidean Gram volume to the
Cayley-Menger volume for realized tetrahedra. -/
def GramCayleyMengerVolumeTheorem : Prop :=
  ∀ T : RealizedTet, volumeSqFromCM T = volumeSqFromGram T

/-- Euclidean oriented volume squared from the Gram determinant:
`V² = det(Gram) / 36`. -/
def volumeSqFromGram (T : RealizedTet) : ℝ :=
  Matrix.det (gram3 T) / 36

/-- Cayley-Menger volume squared from the extracted edge data:
`V² = cm3 / 288`. -/
def volumeSqFromCM (T : RealizedTet) : ℝ :=
  cm3 (sqEdgeOfPoints T) / 288

/-- The defining Gram-volume identity. -/
theorem det_gram3_eq_36_volumeSq (T : RealizedTet) :
    Matrix.det (gram3 T) = 36 * volumeSqFromGram T := by
  unfold volumeSqFromGram
  ring

What this page does not claim

The declaration does not prove the volume identity; it only states it as a target proposition. The declaration does not claim that any six numbers form a valid tetrahedron. The declaration does not address degenerate tetrahedra where the four points are coplanar.

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