rightAngleUnitTet
plain-language theorem explainer
The right-angle unit tetrahedron is packaged as a non-degenerate tetrahedron: all six squared edge lengths are positive and the Cayley–Menger value is positive. Anyone checking the classical identity $288 V^2 = \mathrm{CM}_3(a)$ at a second test point (alongside the regular unit tet) cites this witness. The construction is a structure instance whose two positivity fields are discharged by `fin_cases`/`norm_num` and a named evaluation lemma.
Claim. The right-angle unit tetrahedron, with squared edge lengths given by the standard right-angle unit configuration, is non-degenerate: every squared edge length is strictly positive, and the Cayley–Menger polynomial $\mathrm{CM}_3$ of those six lengths is strictly positive (so the Euclidean volume is real and nonzero).
background
This module builds the analytic substrate for a genuine 3D Regge component theorem $M_{ij}=-\mathrm{area}(f_{ij})$. The first pillar is the Cayley–Menger polynomial $\mathrm{CM}_3$ in the six squared edge lengths $a:\mathrm{Fin},6\to\mathbb{R}$, with the classical volume relation $288 V^2=\mathrm{CM}_3(a)$ checked at concrete test points.
A non-degenerate tetrahedron is a structure carrying squared edges $a$, a proof that every $a_i>0$, and a proof that $\mathrm{CM}_3(a)>0$. The right-angle unit configuration is the second standard test point after the regular unit tetrahedron: three mutually orthogonal unit edges meet at a vertex, and the three face diagonals complete the edge set.
The ambient dimension is the RS-forced $D=3$ (forcing chain T8). Schläfli and dihedral-cosine identities appear later in the same file as named classical hypotheses, not as consequences of this witness.
proof idea
The definition is a structure instance of NonDegenerateTet with squared-edge field set to the right-angle unit edge map. Edge positivity is proved by unfolding that map, casing on the six edge indices, and closing each numeric inequality by norm_num. Volume positivity rewrites the Cayley–Menger evaluation at this configuration via the named lemma cm3_rightAngle_unit, then finishes by norm_num. No geometric construction or derivative work is involved; it is a pure positivity certificate for one fixed point in edge-length space.
why it matters
Module documentation lists regular and right-angle unit tetrahedra as the two test points that verify $288 V^2=\mathrm{CM}_3(a)$ before gradients, Schläfli, and the conditional Regge Hessian theorem are developed. This witness therefore anchors the Euclidean-volume side of the rigorous Regge foundation in $D=3$, the spatial dimension forced by T8.
It does not itself state Schläfli's identity or the off-diagonal claim $M_{ij}=-\mathrm{area}(f_{ij})$; those sit downstream as named external hypotheses and a conditional theorem. With no recorded used_by edges yet, its role is local certification inside the Regge foundation bundle rather than a widely reused lemma. It pairs with the regular unit tetrahedron as the second concrete realisable point on the Cayley–Menger cone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.