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 or edge-length embeddings cite it as the ambient open set on which cofactor ratios stay well-defined. The module is mostly definitional, with two elementary membership lemmas for the regular and right-angled unit tetrahedra.
claimThe open realisable tetrahedral cone consists of squared edge-length 6-tuples $(d_{12}^2,\dots,d_{34}^2)$ with every coordinate positive and Cayley-Menger determinant $\mathrm{CM}_3>0$. The regular unit tetrahedron and the right-angled unit tetrahedron both lie in this cone.
background
A tetrahedron is determined up to congruence by its six edge lengths. The classical 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 positive edge lengths is the first open condition guaranteeing a non-degenerate Euclidean realisation in $\mathbb{R}^3$.
The upstream module CayleyMengerMatrix supplies the explicit polynomial cm3 and the determinant/cofactor layer needed by the dihedral cosine formula. The present module packages the simplest open set on which those cofactors are expected to be non-zero: all squared edges positive and $\mathrm{CM}_3>0$. Later phases add face-minor positivity when denominators in cofactor ratios demand it.
Two concrete points are recorded inside the cone: the regular unit tetrahedron and a right-angled unit tetrahedron. These serve as base cases for continuity and derivative arguments downstream.
proof idea
This is primarily a definition module. The cone is introduced as the set of positive squared-edge 6-tuples with strictly positive Cayley-Menger determinant. Two short membership proofs verify that the regular unit tetrahedron and the right-angled unit tetrahedron satisfy the defining inequalities; both reduce to direct evaluation of the edge list and of cm3. No deep algebraic identities are required at this stage.
why it matters in Recognition Science
The cone is the ambient open set for all subsequent tetrahedral geometry in the Recognition stack. Downstream, CofactorDerivatives imports it to expose derivative hooks for Cayley-Menger cofactors and the dihedral cofactor ratio; those hooks presuppose that one is already inside a region where the relevant denominators do not vanish. In the broader framework the same cone underwrites the passage from abstract edge data to realised 3-space geometry (T8 forces $D=3$), so every later claim about dihedral angles, volume derivatives, or edge-length flows sits over this open set. Strengthening by face-minor positivity is explicitly deferred, keeping the present layer minimal.
scope and limits
- Does not enforce positivity of face minors or 2-face Cayley-Menger determinants.
- Does not prove that every point of the cone embeds as a non-degenerate tetrahedron in R^3 beyond the CM3>0 criterion.
- Does not address oriented volume sign or chirality.
- Does not supply derivative formulae; those live in CofactorDerivatives.
- Does not treat degenerate or flat limits where CM3=0.