Geometry Tetrahedron Realization

Realizing a tetrahedron

A tetrahedron is the simplest three-dimensional solid: four points in space, not all in one plane, joined by six edges and four triangular faces. Its classical study asks which sets of six lengths can form such a shape, and how to compute its volume from those lengths alone. The Cayley-Menger determinant answers the second question with a formula using only the squared edge lengths, and the determinant is zero exactly when the six lengths fail to make a nondegenerate tetrahedron.

In Recognition Science, the framework's machine-checked library of formal theorems treats the same object. The module realizes a tetrahedron, meaning it chooses four actual points in Euclidean three-dimensional space and records the condition that they are not all in one plane. From those points it extracts the six squared edge lengths in a fixed order, then builds the Gram matrix of the three edge vectors meeting at one vertex. The Gram determinant gives the volume squared as det(G)/36, while the Cayley-Menger formula gives it as cm/288.

The module proves these two volume expressions agree for every realized tetrahedron. The key theorem states that the Cayley-Menger volume squared equals the Gram volume squared for all nondegenerate tetrahedra. The proof is a direct computation: the library defines the Cayley-Menger determinant from the six squared edges, defines the Gram determinant from the point coordinates, and shows the two are equal by expanding both formulas. This bridges the abstract edge-data layer to concrete geometry.

This agreement matters because the six squared edge lengths are what a discrete ledger of recognition events would record, while the Gram determinant is what ordinary Euclidean geometry computes from points. The theorem shows the two descriptions cannot diverge for any actual tetrahedron. It is a foundational check that the edge-based language carries the same volume information as the point-based language, so later results about dihedral angles and positive volume can rely on either representation.

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

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

/-- Squared edge lengths from points are nonnegative. -/
theorem sqEdgeOfPoints_nonneg (T : RealizedTet) (e : Fin 6) :
    0 ≤ sqEdgeOfPoints T e := by
  unfold sqEdgeOfPoints vertexSqDist
  exact sq_nonneg _

What this page does not claim

This module does not prove that every set of six nonnegative lengths forms a tetrahedron. It does not derive the dihedral angle bounds or positive volume for degenerate cases. It does not connect the tetrahedron realization to the forcing chain that yields three spatial dimensions.

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: