Geometry Tetrahedron Realization Volume Sq From Gram

Volume from edge data

A tetrahedron is a solid with four triangular faces, six edges, and four vertices. In Euclidean geometry, its volume is determined completely by the six edge lengths, a fact formalized in the Cayley-Menger determinant. The declaration volumeSqFromGram expresses one route to that volume: take three edge vectors meeting at a single vertex, form their 3 by 3 matrix of dot products (the Gram matrix), and divide its determinant by 36. The result is the square of the ordinary volume, so the formula reads V² = det(Gram) / 36.

The classical background is worth stating plainly. For any tetrahedron placed in three-dimensional space, this Gram-determinant identity is a standard result of linear algebra, not a new discovery. The same volume can also be written through the Cayley-Menger determinant, which uses only the six squared edge lengths directly. The framework's library, a machine-checked collection of formal theorems, contains both definitions and a theorem stating that the determinant of the Gram matrix equals 36 times the squared volume from Gram. That identity is proved by unfolding the definition and applying the ring tactic; it is a formal theorem, not an assumption.

In Recognition Science, this declaration plays a supporting role. The framework models a tetrahedron as a structure holding four points in Euclidean 3-space together with an affine-independence condition, which rules out degenerate flat configurations. From those points it defines edge vectors, squared distances, and the Gram matrix. The squared-volume-from-Gram definition is one step in a larger project: connecting the abstract six squared-edge coordinates used by the Cayley-Menger layer to actual points in space. The theorem target named GramCayleyMengerVolumeTheorem states that for every realized tetrahedron, the Cayley-Menger volume squared equals the Gram volume squared. That target is a declared proposition, not yet proved in the pack.

What the declaration does not claim is as important as what it proves. It does not assert that any six positive numbers form a tetrahedron; the affine-independence condition is a separate hypothesis. It does not prove the Cayley-Menger volume equals the Gram volume, because that equality remains an open target. It does not establish that the volume is positive, since the definition allows the determinant to be zero or negative in principle. The declaration is a definition with one proved identity attached, not a complete theory of tetrahedral volume.

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

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

Not claimed: that any six positive numbers form a tetrahedron. Not claimed: that the Cayley-Menger volume equals the Gram volume, which remains an open target. Not claimed: that the squared volume from Gram is always positive.

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: