Geometry Tetrahedron Realization Realized Tet

The realized tetrahedron

A tetrahedron is the simplest three-dimensional solid: four points, not all in one plane, joined by six edges and four triangular faces. The classical definition asks for points in ordinary Euclidean space. The Recognition Science structure RealizedTet (a machine-checked object in the framework's library of formal theorems) packages precisely that: it holds four points in Euclidean 3-space and a proof that they are affinely independent, meaning they do not all lie in a single plane.

From those four points the structure extracts the six squared edge lengths, the three edge vectors meeting at one vertex, and their Gram matrix of inner products. Two volume formulas arise. The Gram determinant gives V² = det(Gram)/36, and the classical Cayley-Menger determinant gives V² = cm3/288 from edge data alone. A theorem in the same module states that for any realized tetrahedron these two volumes agree, connecting the point-based picture to the edge-based one.

In Recognition Science, this structure is groundwork, not a headline. The framework's larger program derives physical constants and dimensions from a cost function, but RealizedTet is a geometric bridge: it ties abstract six-number edge data to concrete points, ready for later proofs about dihedral angles and positive volume. The nondegenerate field is kept explicitly as the hypothesis that will feed those future results.

What RealizedTet does not claim is just as important. It does not assert that every six numbers satisfying the Cayley-Menger conditions correspond to a tetrahedron; that embedding question is a separate theorem. It does not prove the volume equality for all edge data, only for data already realized by points. And it says nothing about the framework's forcing chain, golden ratio, or physical constants. It is a precise, modest tool: a definition and a few supporting lemmas, ready for heavier work.

/-- A tetrahedron realized by four points in Euclidean 3-space.  The
`nondegenerate` field is kept as the affine-independence hypothesis that
will later feed the strict dihedral range and positive-volume proofs. -/
structure RealizedTet where
  p : Fin 4 → EuclideanSpace ℝ (Fin 3)
  nondegenerate : AffineIndependent ℝ p

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

What this page does not claim

RealizedTet does not prove that every six numbers satisfying the Cayley-Menger conditions correspond to a tetrahedron. It does not derive the golden ratio, physical constants, or any part of the forcing chain. It does not assert the volume equality for edge data that are not realized by points.

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: