star_cm3
plain-language theorem explainer
The Cayley-Menger polynomial of the one-parameter star tetrahedron (squared edges 1,1,1,1,1,p) equals 2p(3-p). Anyone certifying Euclidean realizability of the four-tet hinge star cites this algebraic identity. The proof substitutes the six edge values into the explicit CM polynomial and closes by ring.
Claim. For every real $p$, if $a$ is the squared-edge 6-tuple with $a_0=a_1=a_2=a_3=a_4=1$ and $a_5=p$, then the Cayley-Menger polynomial satisfies $\mathrm{CM}_3(a)=2p(3-p)$. The identity holds for all real $p$; geometric nondegeneracy requires the open interval $0<p<3$.
background
This module builds signed Regge-convention deficit angles on an abstract four-tetrahedron hinge star: four congruent tets share an interior hinge AB in a closed 4-cycle link. Squared edges are locked to the panel $(l,m,m,m,m,p)$; the kernel-checked slice is $l=m=1$, so the edge vector is $(1,1,1,1,1,p)$ with hinge edge 0.
The Cayley-Menger polynomial $\mathrm{CM}_3$ is the explicit degree-3 polynomial in the six squared edge lengths whose sign is the standard determinantal certificate that a 6-tuple is realizable as a nondegenerate Euclidean tetrahedron. Upstream, cm3 is defined by the expanded formula
$2\bigl(a_0 a_5(a_1+a_2+a_3+a_4-a_0-a_5)+\cdots\bigr)$ (six quadratic terms minus four cubic monomials).
The star edge map simply writes the constant-1 rim with free equatorial squared length $p$. Flat closure of the 4-cycle sits at $p_0=3/2$; the deformation $p(h)=(3/2)(1-h)$ later makes the common dihedral cosine equal $h$ on the nose.
proof idea
Term-mode style via six reflexivity facts: the star edge map evaluates to 1 on indices 0 through 4 and to $p$ on index 5. Unfold the explicit Cayley-Menger polynomial, rewrite those six components in, and finish with ring. No external lemmas beyond the definitions of the edge map and $\mathrm{CM}_3$; the identity is pure polynomial arithmetic.
why it matters
Direct parent is the nondegeneracy certificate: for $|h|<1$ the deformed star has $\mathrm{CM}_3>0$, proved by rewriting through this identity and two linear inequalities on $p(h)$. That certificate is the Euclidean-realizability gate for the whole four-tet signed-deficit development: once $\mathrm{CM}_3>0$, the common dihedral cosine $q=(3-2p)/3$ is well-defined, the deficit equals $4\arcsin(h)$, and the sign of the deficit is the sign of the rational parameter $h$ with no arccos or interval arithmetic.
In the broader Recognition geometry stack this is the first kernel-checked signed Regge deficit on an abstract hinge star. It sits downstream of the Cayley-Menger polynomial and cofactor infrastructure and upstream of weak-field mesh bounds on the deficit. It does not yet touch the continuum bridge or Hamiltonian emergence layers; those consume the signed deficit only after the local star is certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.