fourTet_nondegenerate
plain-language theorem explainer
For deformation parameter |h| < 1, the one-parameter star tetrahedron (hinge and spokes squared length 1, rim p = (3/2)(1-h)) has strictly positive Cayley-Menger polynomial. Anyone citing Euclidean realizability of the four-tet hinge star needs this certificate. The proof rewrites cm3 via the closed form 2p(3-p) and checks 0 < p < 3 by linear arithmetic on |h| < 1.
Claim. If $|h| < 1$, then the Cayley-Menger polynomial of the star tetrahedron with squared edges $(1,1,1,1,1,p(h))$, where $p(h) = \frac{3}{2}(1-h)$, is strictly positive: $\mathrm{cm}_3 > 0$.
background
The module builds signed Regge deficit angles on an abstract four-tetrahedron hinge star: four congruent tets share an interior hinge AB in a closed 4-cycle link. Squared-edge data are locked to hinge and spoke lengths 1 with variable rim length $p$, written as the vector $(1,1,1,1,1,p)$. The deformation family is $p(h) = \frac{3}{2}(1-h)$, so the flat configuration sits at $h = 0$ ($p = 3/2$), where the common dihedral cosine at the hinge vanishes.
The Cayley-Menger polynomial $\mathrm{cm}_3$ is the explicit degree-3 determinant polynomial in the six squared edge lengths; its strict positivity is the classical algebraic certificate that the edge data realize a nondegenerate Euclidean tetrahedron (volume squared proportional to $\mathrm{cm}_3$). Upstream, star_cm3 evaluates this polynomial on the star family to the elementary identity $\mathrm{cm}_3 = 2p(3-p)$, positive exactly on the open interval $0 < p < 3$.
proof idea
Unpack $|h| < 1$ into $-1 < h < 1$. Rewrite the goal by the identity $\mathrm{cm}_3(\mathrm{starSq},p) = 2p(3-p)$. Two short nlinarith steps show $0 < p(h)$ and $p(h) < 3$ from the bounds on $h$ and the definition $p(h) = \frac{3}{2}(1-h)$. A final nlinarith closes $2p(3-p) > 0$. No cofactor or dihedral machinery is used; the argument is pure polynomial positivity on the open rim interval.
why it matters
Nondegeneracy is the gate for every geometric reading of the four-tet star. Downstream, fourTet_weak_pair (the weak-field signed-pair certificate, Test B) invokes it to guarantee that both configurations at deformation parameters $\pm h^2$ remain Euclidean tetrahedra while carrying opposite-sign deficits $\mathrm{deficit}(-h^2) = -\mathrm{deficit}(+h^2)$ with rational hinge cosines $\pm h^2$.
In the module's design, the signed deficit is $4\arcsin(h)$ once the cosine is identified with $h$, so the sign of curvature is read off a rational quantity without arccos or interval arithmetic. This lemma supplies the missing $\mathrm{cm}_3 > 0$ half of that package in the open unit interval for $h$. It does not itself address continuum Regge calculus or a full triangulation; it is the local algebraic license for the abstract star used throughout the signed-deficit development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.