regularUnit_mem_realisableTetCone

The module fixes the open domain on which tetrahedral Cayley-Menger and dihedral-angle formulas are meant to run. Squared edge data are 6-tuples $a : \mathrm{Fin},6 \to \mathbb{R}$. The basic realisability cone is the open set of those $a$ with every component strictly positive and with Cayley-Menger determinant $\mathrm{cm}_3(a) > 0$. Later phases may add face-minor positivity for cofactor denominators; the present cone is only the two inequalities above.

The regular unit edge vector is the constant map $a_i = 1$. Classically the unit regular tetrahedron has volume $\sqrt{2}/12$, so $288 V^2 = 4$. That identity is already recorded as $\mathrm{cm}_3(\mathrm{regular,unit}) = 4$, which supplies the second cone inequality once the first is checked.

Cone membership is a conjunction, so the proof opens with constructor. The edge-positivity goal unfolds the constant-1 edge map and finishes by norm_num on each of the six coordinates. The Cayley-Menger goal rewrites by the upstream evaluation $\mathrm{cm}_3 = 4$ for the regular unit and again closes by norm_num. No geometric construction is needed beyond those two algebraic facts.

Without a certified interior point, the open domain for tetrahedral Cayley-Menger and dihedral formulas is only a formal set. This theorem places the classical regular unit tetrahedron inside that domain, so every subsequent identity that assumes cone membership can be instantiated on a concrete, physically standard tetrahedron. The sibling right-angle unit tetrahedron plays the same role for an orthogonal edge configuration. In the broader Recognition geometry stack the cone is the ambient set for Regge-style hinge and deficit analysis; a nonempty open cone is the minimal sanity check before those formulas are applied. No downstream consumers are wired yet, so the result presently anchors the module rather than a larger forcing step.