regularUnitTet
plain-language theorem explainer
The unit regular tetrahedron (all six edges of length 1) is recorded as a non-degenerate tetrahedron: positive squared edge lengths and positive Cayley-Menger value. Dihedral-angle and cofactor lemmas cite it as the canonical regular test point. The body is a structure instance whose two positivity fields discharge by norm_num after the identity CM₃ = 4.
Claim. The regular tetrahedron with all squared edge lengths equal to $1$ is non-degenerate: every squared edge length is strictly positive, and its Cayley-Menger polynomial satisfies $\mathrm{CM}_3 > 0$ (classically $\mathrm{CM}_3 = 4$, so $288 V^2 = 4$).
background
The module builds the analytic substrate for a genuine 3D Regge component theorem $M_{ij} = -\mathrm{area}(f_{ij})$. It packages the Cayley-Menger polynomial $\mathrm{CM}_3$ in the six squared edge lengths, its gradient and Taylor identity, and named classical hypotheses (Schläfli, dihedral cofactors, smoothness on the realisability cone).
A non-degenerate tetrahedron is a structure carrying squared-edge data $a:\mathrm{Fin},6\to\mathbb{R}$ with $a_i>0$ for all $i$ and $\mathrm{CM}_3(a)>0$. The unit regular edge data is the constant map $a\equiv 1$. Upstream, $\mathrm{CM}_3(a)=4$ for that data, matching the classical volume $V=\sqrt{2}/12$ via $288 V^2=4$.
proof idea
Structure instance of the non-degenerate-tetrahedron type. Squared edges are set to the constant unit regular data. Edge positivity is intro then unfold of that constant map and norm_num. Cayley-Menger positivity rewrites by the upstream identity $\mathrm{CM}_3=4$ and finishes with norm_num.
why it matters
Supplies the standard regular test tetrahedron used throughout the dihedral Cayley-Menger layer. Downstream, the cofactor cosine on this object equals $1/3$, and the cofactor angle matches the existing regular-tetrahedron dihedral API, both unconditionally once the regular cofactor check is in place. That calibration sits inside the Regge foundation path toward the conditional component theorem $M_{ij}=-\mathrm{area}(f_{ij})$ under the conformal edge ansatz, with Schläfli and cofactor formulae imported as named classical hypotheses rather than RS-derived facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.