star_q
plain-language theorem explainer
Along the one-parameter family of squared rim lengths p(h)=(3/2)(1-h), the Cayley–Menger hinge dihedral cosine of the abstract four-tet star equals h exactly. Anyone citing the signed Regge deficit or the weak-field pair on this star uses this identity as the rational certificate. The proof rewrites by the l=m=1 cosine formula, unfolds p(h), and finishes by ring.
Claim. For every real $h$, if the star tetrahedron has squared edges $(1,1,1,1,1,p)$ with rim length $p=(3/2)(1-h)$, then the Cayley–Menger dihedral cosine at the hinge edge equals $h$. (A cosine reading needs $|h|\le 1$; nondegeneracy needs $|h|<1$.)
background
The module builds signed Regge deficits on an abstract four-tetrahedron hinge star: four congruent tets share an interior edge AB in a closed 4-cycle link. Squared-edge data are locked to hinge and spoke lengths 1 and variable rim length $p$, written $(a_0,\ldots,a_5)=(1,1,1,1,1,p)$ with hinge edge 0. Nondegeneracy is the Cayley–Menger sign $\mathrm{cm}_3>0$, not a full triangulation embedding.
The dihedral cosine is the repository cofactor formula dihedralCos3Sq. On the slice $l=m=1$, the upstream theorem fourTet_centralDihedralCosine gives the rational identity $q(p)=(3-2p)/3$. The flat rim is $p_0=3/2$ (where $q=0$, so each dihedral is $\pi/2$). The deformation family is $p(h)=(3/2)(1-h)$, so that $q$ tracks $h$ on the nose and the sign of the deficit is the sign of a rational quantity.
Deficit itself is the usual Regge quantity $2\pi-\sum\theta$, with each angle $\arccos$ of the cofactor cosine.
proof idea
One short algebraic chain. Rewrite the left-hand side by fourTet_centralDihedralCosine, which replaces the cofactor cosine on starSq p by the rational $(3-2p)/3$. Unfold starP to substitute $p=(3/2)(1-h)$. A single ring reduces $(3-2\cdot(3/2)(1-h))/3$ to $h$. No arccos, no inequalities, no nondegeneracy hypotheses enter the identity.
why it matters
This is the rational certificate that turns the deformation parameter into the hinge cosine, so deficit sign is read off without transcendental evaluation. Downstream, fourTet_deficit_eq rewrites the star deficit as $2\pi-4\arccos(h)$ by applying this identity inside the angle definition. The weak-field pair theorem fourTet_weak_pair (Test B certificate) then instantiates at $\pm h^2$ to get opposite-sign deficits, exact antisymmetry, and explicit mesh bounds in the weak regime.
In the module narrative this closes the kernel-checked path from squared-edge data through cofactors to a signed Regge deficit on a four-tet star, the first such object in the repository. It sits in the geometry layer that supports hinge-aware Regge analysis; it does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law, but supplies the local curvature sign control those continuum limits need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.