Geometry Tetrahedron Realization Gram3 Symm

The Gram symmetry

A tetrahedron is a pyramid with four triangular faces. Place its four corners anywhere in ordinary three-dimensional space, pick one corner as the base, and draw the three edge vectors from it to the other three corners. The Gram matrix collects the dot products of these three vectors: the entry in row i and column j is the dot product of the i-th and j-th edge vectors. For any such tetrahedron, that matrix is symmetric: the entry in row i and column j equals the entry in row j and column i. The reason is that a dot product does not care about order; the dot product of vector a with vector b is the same number as the dot product of b with a. This symmetry is what the declaration gram3_symm establishes.

The statement is a theorem in the machine-checked library of formal theorems of the Recognition Science framework. It is proved for every realized tetrahedron, meaning any four points in Euclidean 3-space that are affinely independent, so they do not all lie in a single plane. The proof is one line: it unfolds the definition of the Gram matrix and applies the commutativity of the real inner product. The theorem is not about a particular tetrahedron; it holds for all of them. This symmetry is the first step toward a larger goal: connecting the six squared edge lengths of a tetrahedron to its volume. The same Gram matrix also appears in the classical formula for the squared volume of a tetrahedron, V² = det(Gram) / 36, where det is the determinant.

The symmetry itself is a classical fact of Euclidean geometry, known for centuries and used throughout mathematics. What the framework adds is a formal, machine-checked proof that the fact holds in its own construction of Euclidean space. The declaration does not claim that the Gram matrix is positive definite, that the tetrahedron has positive volume, or that the Cayley-Menger volume formula agrees with the Gram volume formula. Those are separate targets, some already stated as future theorems in the same module. The symmetry alone says nothing about the size or shape of the tetrahedron; it only says that the matrix of dot products is symmetric, which is a necessary condition for any Gram matrix of real vectors.

In Recognition Science, this symmetry is a small but load-bearing piece of the bridge between abstract edge-length data and actual points in space. The framework models a tetrahedron by its six squared edge lengths, and the Gram matrix is how those lengths become coordinates. The symmetry guarantees that the matrix is well-behaved enough to talk about its determinant, which leads to volume. Without symmetry, the Gram determinant would not be a meaningful volume. So this one-line theorem is the hinge that lets the framework move from a list of six numbers to a solid object with a volume.

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

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

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

What this page does not claim

This theorem does not claim that the Gram matrix is positive definite or that the tetrahedron has positive volume. This theorem does not claim that the Cayley-Menger volume formula agrees with the Gram volume formula. This theorem does not claim anything about the size or shape of the tetrahedron beyond the symmetry of its Gram matrix.

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: