Geometry Tetrahedron Realization Basis Edge Vector

The edge basis

A tetrahedron is a pyramid with four triangular faces. In Euclidean 3-space, four points that are not all in one plane determine such a solid. The Recognition Science framework's declaration basisEdgeVector (a coined term for the three edge vectors from a chosen vertex) picks out the three vectors from vertex 0 to the other three vertices, which together span the whole tetrahedron.

Classically, any tetrahedron can be described by its six edge lengths. The framework's module connects that abstract description to actual points in Euclidean space. The declaration RealizedTet (a structure holding four points in Euclidean 3-space) carries a nondegeneracy condition, meaning the four points are affinely independent, so they do not collapse into a plane or a line. From such a realized tetrahedron, the declaration edgeVector (the difference of two vertex positions) gives the vector along any edge, and basisEdgeVector collects the three vectors from vertex 0 to vertices 1, 2, and 3.

These three vectors form a basis of the ambient 3-dimensional space precisely when the tetrahedron is nondegenerate. The framework uses them to build a 3 by 3 Gram matrix of inner products, whose determinant relates to the squared volume by the classical formula V² = det(Gram)/36. A proved theorem in the framework's machine-checked library of formal theorems states that this determinant equals 36 times the volume squared, and another theorem states that the Gram matrix is symmetric. These are formal, kernel-checked results about real Euclidean geometry.

What the declaration does not claim is more important than what it does. It does not assert that any six positive numbers form a tetrahedron; that is a separate realizability question, governed by the Cayley-Menger conditions. It does not claim that the three basis vectors are orthogonal or of unit length, only that they span. And it does not, by itself, prove the volume formula from edge lengths alone; that is the target of the GramCayleyMengerVolumeTheorem, which remains a stated goal in the framework, not a proved result.

/-- The three edge vectors from vertex `0` that span the tetrahedron. -/
def basisEdgeVector (T : RealizedTet) : Fin 3 → EuclideanSpace ℝ (Fin 3)
  | 0 => edgeVector T 0 1
  | 1 => edgeVector T 0 2
  | 2 => edgeVector T 0 3

/-- 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 Gram matrix is symmetric. -/
theorem gram3_symm (T : RealizedTet) (i j : Fin 3) :
    gram3 T i j = gram3 T j i := by
  unfold gram3
  rw [real_inner_comm]

What this page does not claim

The declaration does not prove that any six edge lengths determine a tetrahedron. The three basis vectors are not claimed to be orthogonal or unit length. The Gram-Cayley-Menger volume equality is a stated target, not a proved theorem.

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: