Geometry Tetrahedron Realization Det Gram3 Eq 36 Volume Sq

The Gram volume identity

A tetrahedron is a pyramid with a triangular base, four vertices and six edges. In Euclidean 3-space, one can place its four points and measure the squared length of each edge. A classical fact, known since the 19th century, connects these edge lengths to the solid's volume: the square of the volume is a rational function of the six squared edge lengths, given by the Cayley-Menger determinant divided by 288.

The declaration det_gram3_eq_36_volumeSq establishes a different but equivalent route to the same volume. Instead of using all six edges at once, pick one vertex and consider the three edge vectors that start there. The Gram matrix of these three vectors is the 3 by 3 table of their pairwise dot products. The theorem states that the determinant of this Gram matrix equals 36 times the square of the volume of the tetrahedron. In symbols: det(Gram) = 36 V².

This identity is proved for any tetrahedron realized by four points in Euclidean 3-space, with the single condition that the four points are affinely independent, meaning they do not lie in a common plane. The proof is a short algebraic manipulation: the volume squared is defined as det(Gram) / 36, so the equality holds by definition and the ring axiom. The theorem is a machine-checked statement in the framework's library of formal theorems, carrying the tag THEOREM.

What this declaration does not claim is more interesting than what it proves. It does not assert that the Gram determinant is positive; that requires the affine-independence hypothesis to be strengthened into a strict inequality, which the module leaves as a later target. It does not connect the Gram volume to the Cayley-Menger formula; that connection is a separate, unproved target named GramCayleyMengerVolumeTheorem. And it says nothing about the Recognition Science framework's larger claims, such as the forcing of three spatial dimensions; this is a standalone piece of Euclidean geometry, not a step in that chain.

The practical payoff is a clean bridge between two ways of measuring a tetrahedron: one from a vertex and its three incident edges, the other from all six edge lengths. The identity lets a computation switch between these representations without loss, which is the kind of lemma that later volume and dihedral-angle proofs will build on.

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

/-- 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 theorem does not prove that the Gram determinant is positive for nondegenerate tetrahedra. The theorem does not establish equality between the Gram volume and the Cayley-Menger volume. The theorem is not part of the framework's chain forcing 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: