IndisputableMonolith.Geometry.TetrahedronRealization
Four points in Euclidean 3-space realize a tetrahedron, with affine independence kept as nondegeneracy. The module builds edge vectors, the 3×3 Gram matrix of a basis triple, and squared volume from both the Gram determinant and the Cayley–Menger polynomial. Anyone comparing Euclidean embeddings to edge-length data in 3D Regge calculus would cite it. Content is definitions plus elementary Gram and determinant identities.
claimA realized tetrahedron is four points $p_0,p_1,p_2,p_3\in\mathbb{R}^3$ that are affinely independent. Edge vectors $v_i=p_i-p_0$ yield the Gram matrix $G_{ij}=v_i\cdot v_j$, with $\det G=36 V^2$. Squared volume is also recovered from the Cayley–Menger polynomial in the six squared edge lengths.
background
This module sits in the geometry layer that underwrites a rigorous 3D Regge component theorem. Upstream, the Cayley–Menger polynomial module writes an explicit degree-3 polynomial in the six squared edge lengths of a tetrahedron, aimed at comparing the genuine Regge second-variation matrix $M_{ij}$ componentwise to face areas. The Regge foundation module bundles that polynomial and related identities needed for $M_{ij}=-\mathrm{area}(f_{ij})$.
Here the tetrahedron is realized concretely: four points in Euclidean 3-space, with a nondegeneracy field recording affine independence (later used for strict dihedral ranges and positive volume). From a base vertex one forms three edge vectors, their Gram matrix, and squared volume via $\det G/36$. Squared edge lengths of the embedded points feed the Cayley–Menger side of the same volume formula.
Mathlib supplies the Euclidean and $\ell^2$ inner-product infrastructure and matrix determinants; the RS geometry imports supply the polynomial and Regge scaffolding.
proof idea
Definition-first module. It packages a realized tetrahedron structure (four points plus affine independence), edge-vertex indexing, edge vectors, and squared distances between vertices. The Gram matrix of the three basis edge vectors is defined and shown symmetric. Squared volume is extracted as $\det G/36$, with a lemma equating $\det G$ to $36$ times that quantity. A parallel Cayley–Menger volume-squared expression is exposed for comparison. No deep existence or classification proof; the work is wiring Euclidean data to the edge-length polynomial already defined upstream.
why it matters in Recognition Science
The module is the Euclidean embedding half of the Gram–Cayley–Menger bridge. Downstream, GramCayleyMenger isolates the theorem that the Gram determinant of a realized tetrahedron equals (a fixed multiple of) its Cayley–Menger determinant. That identity is the concrete link between an embedded simplex in $\mathbb{R}^3$ and the pure edge-length calculus used in Regge calculus.
In the broader RS geometry program this feeds the rigorous path to the Regge component relation $M_{ij}=-\mathrm{area}(f_{ij})$: second variations and dihedral derivatives must match face areas once volume and angle formulae are under control. Affine independence kept on the realization is the hypothesis later used for positive volume and strict dihedral ranges. Landmark contact is local (3-space tetrahedra, $D=3$ geometry), not the forcing chain T0–T8 itself.
scope and limits
- Does not prove the Regge identity $M_{ij}=-\mathrm{area}(f_{ij})$.
- Does not construct or classify all metric tetrahedra; it assumes four points in $\mathbb{R}^3$.
- Does not derive dihedral-angle formulae or second-variation matrices.
- Does not assert uniqueness of the embedding up to isometry beyond the data given.
- Does not close the full Gram–Cayley–Menger equality; that lives downstream.