RealisableTetCone
plain-language theorem explainer
The basic open realisability cone for a tetrahedron: six-tuples of squared edge lengths that are strictly positive and give a strictly positive Cayley-Menger determinant. Geometry and dihedral-angle work in the Recognition stack cites it as the open domain of those formulas. Pure set definition by two positivity constraints; later phases add face-minor conditions.
Claim. The realisable tetrahedral cone is the set of squared-edge 6-tuples $a=(a_0,\ldots,a_5)$ such that $a_i>0$ for every index $i\in\{0,\ldots,5\}$ and the Cayley-Menger polynomial $\mathrm{cm}_3(a)$ is strictly positive.
background
This module fixes the open domain on which tetrahedral Cayley-Menger and dihedral-angle formulas are meant to run. A configuration is a 6-tuple of squared edge lengths (type SqEdges), one entry per edge of $K_4$.
The Cayley-Menger polynomial $\mathrm{cm}_3$ is the explicit degree-3 polynomial in those six squared lengths whose value is proportional to the squared volume of a tetrahedron with those edges. Strict positivity of $\mathrm{cm}_3$ is the classical open condition for positive volume (non-degenerate embedding in $\mathbb{R}^3$ up to congruence).
The cone here is deliberately minimal: componentwise positivity of the squared edges, plus $\mathrm{cm}_3>0$. The module doc notes that later phases may add face-minor positivity when cofactor denominators require it.
proof idea
Definition by set comprehension, not a theorem. A 6-tuple $a$ lies in the cone exactly when both conjuncts hold: every coordinate $a_i$ is positive, and $\mathrm{cm}_3(a)>0$. Two one-line projection lemmas unpack membership into those two facts.
why it matters
Gives the ambient open set for all subsequent tetrahedral realisability statements in this module. Immediate consumers prove that the regular unit tetrahedron and the right-angle unit tetrahedron both sit inside the cone, so the basic geometric test cases are admissible for Cayley-Menger and dihedral formulas.
In the broader Recognition geometry layer this is scaffolding for volume and angle identities on discrete tetrahedra, not yet tied to the forcing chain (T0-T8) or the mass ladder. The doc-comment flags the planned strengthening: face-minor positivity for cofactor denominators. Until that lands, any formula that divides by a face minor must either stay inside a stricter subdomain or carry an extra hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.