IndisputableMonolith.Geometry.RealisabilityCone
Defines the basic open realisability cone for a tetrahedron: six positive squared edge lengths together with a strictly positive Cayley-Menger determinant. Geometers working on dihedral angles and cofactor ratios cite it as the open set on which those formulae are well-defined. Membership lemmas place the regular unit tetrahedron and a right-angled unit tetrahedron inside the cone.
claimThe open realisability cone $\mathcal{R}_{\mathrm{tet}}$ consists of squared edge-length 6-tuples $(d_{12}^2,\ldots,d_{34}^2)\in\mathbb{R}_{>0}^6$ for which the Cayley-Menger determinant $\mathrm{CM}_3>0$. The regular unit tetrahedron and a right-angled unit tetrahedron both lie in $\mathcal{R}_{\mathrm{tet}}$.
background
In classical distance geometry a tetrahedron is determined (up to congruence) by its six edge lengths. The Cayley-Menger determinant $\mathrm{CM}_3$ of the associated $5\times 5$ bordered matrix of squared distances vanishes precisely when the four points are coplanar; positivity of $\mathrm{CM}_3$ together with positivity of the squared lengths is the first open condition guaranteeing a non-degenerate embedding in $\mathbb{R}^3$.
The upstream module CayleyMengerMatrix supplies the explicit polynomial cm3 and identifies it with the determinant of that matrix, along with the cofactor layer needed for dihedral cosines. The present module packages the elementary open set on which those expressions live: all six squared edges positive and $\mathrm{CM}_3>0$. Later phases are expected to add face-minor positivity so that cofactor denominators never vanish.
proof idea
Definition module. The cone is introduced as a set of positive squared-edge 6-tuples with strictly positive Cayley-Menger determinant. Two short membership lemmas verify that the regular unit tetrahedron and a canonical right-angled unit tetrahedron satisfy the defining inequalities; both reduce to direct evaluation of the squared lengths and of cm3.
why it matters in Recognition Science
Cofactor ratios and their derivatives (module CofactorDerivatives) are only meaningful on an open set where edge lengths are positive and the Cayley-Menger determinant does not vanish. This cone is that ambient open set. Downstream calculus hooks for dihedral cofactors therefore import it as the domain on which symbolic differentiation is legitimate. Within the broader Recognition geometry stack it is the first geometric filter before face-minor strengthenings required by denominator control.
scope and limits
- Does not enforce positivity of face Cayley-Menger minors.
- Does not prove uniqueness or rigidity of the embedded tetrahedron.
- Does not address oriented volume sign or chirality.
- Does not yet supply the cofactor-denominator non-vanishing lemmas.