rightAngleUnit_mem_realisableTetCone
plain-language theorem explainer
The right-angle unit tetrahedron (three orthogonal unit legs from one vertex) sits in the open realisability cone: all six squared edges are positive and the Cayley–Menger determinant equals 8. Anyone working with tetrahedral volume or dihedral formulas on squared-edge data can cite this as a concrete interior point. The proof is a direct membership check: edge positivity by case split, then the known evaluation cm3 = 8.
Claim. Let $a$ be the squared-edge 6-tuple of the right-angle unit tetrahedron (three mutually orthogonal unit edges from one vertex, with the three face diagonals of squared length $2$). Then $a$ lies in the basic realisability cone: $a_i > 0$ for all six edges and the Cayley–Menger determinant satisfies $\mathrm{cm}_3(a) > 0$.
background
The module fixes the open domain on which tetrahedral Cayley–Menger and dihedral-angle formulas are meant to run. Squared-edge data live in SqEdges (maps from six edge indices to reals). The basic realisability cone is the set of such 6-tuples with every coordinate strictly positive and with strictly positive Cayley–Menger determinant $\mathrm{cm}_3$. Later phases may add face-minor positivity for cofactor denominators; this cone is the minimal open set.
The right-angle unit tetrahedron is the classical corner tetrahedron with three orthogonal unit legs from one vertex. Its squared-edge vector therefore has three 1's on the legs and three 2's on the face diagonals. Upstream, the Cayley–Menger polynomial evaluates to 8 on this vector, matching the classical identity $288 V^2 = 8$ for volume $V = 1/6$.
proof idea
Membership in the cone is a conjunction. The first conjunct (all six squared edges positive) is discharged by unfolding the right-angle unit edge map and splitting on the six Fin 6 indices; each case is a numerical positivity check. The second conjunct rewrites the Cayley–Menger value via the upstream evaluation theorem that $\mathrm{cm}_3$ of this edge vector equals 8, then closes by norm_num ($8 > 0$). No geometric construction is rebuilt inside the proof.
why it matters
This supplies a concrete interior point of the tetrahedral realisability cone, parallel to the regular-unit membership sibling in the same module. Downstream consumers of Cayley–Menger volume or dihedral formulas need at least one verified open point before continuity or smoothness arguments can be anchored; the right-angle unit tetrahedron is the standard orthogonal test case (classical $V = 1/6$). In the broader Recognition geometry stack it certifies that the squared-edge domain used for rigid tetrahedra is nonempty and contains the orthogonal configuration that often appears in coordinate charts. No parent theorem currently lists this declaration as a dependency, so it functions as a seed witness rather than a link in a longer forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.