fourTet_deficit_eq
plain-language theorem explainer
On the one-parameter four-tetrahedron hinge star, the star-local Regge deficit equals $2\pi - 4\arccos(h)$, where $h$ is the deformation parameter and also the common hinge dihedral cosine. Anyone working signed Regge deficits or weak-field curvature signs on this abstract star cites this identity. The proof unfolds the deficit definition and substitutes the already-proved cosine identity $q=h$.
Claim. For every real $h$, the star-local Regge deficit of the four-tet hinge star along the deformation family equals $2\pi - 4\arccos(h)$. Equivalently, if four congruent tetrahedra meet at the hinge with common dihedral cosine equal to $h$, then the deficit $2\pi$ minus four times that dihedral angle is $2\pi - 4\arccos(h)$.
background
The module studies an abstract four-tetrahedron hinge star: squared-edge data for four congruent tets around a common hinge AB, certified nondegenerate by Cayley-Menger sign, not a full triangulation embedding. Edges are locked to $|AB|^2=l$, equatorial legs $m$, and opposite edge $p$; the kernel-checked slice is $l=m=1$ with deformation $p(h)=(3/2)(1-h)$.
The star-local deficit is defined as $2\pi$ minus four copies of the repository dihedral angle on that squared-edge data (hinge edge 0). Dihedral angle is $\arccos$ of the Cayley-Menger cofactor cosine. Upstream, star_q proves that along this family the hinge cosine equals $h$ exactly (as a real identity; geometric cosine reading needs $|h|\le 1$). The classical deficit convention is the same $2\pi-\sum\theta$ used elsewhere in the geometry stack.
proof idea
Term-mode, three steps. Unfold the star deficit to $2\pi - 4\cdot\mathrm{dihedralAngle3Sq}(\mathrm{starSq}(\mathrm{starP},h),0)$, then unfold dihedral angle to $\arccos$ of the squared-edge cosine. Rewrite the cosine by the identity that it equals $h$ on the nose. The goal collapses to $2\pi - 4\arccos(h)$ with no further arithmetic.
why it matters
This is the closed arccos form of the signed four-tet star deficit, the bridge from squared-edge data to an elementary transcendental expression in the deformation parameter. Downstream, the arcsin rewrite uses it plus the standard $\arccos x = \pi/2 - \arcsin x$ identity to obtain $\mathrm{deficit}(h)=4\arcsin(h)$, so the sign of the deficit is the sign of the rational $h$ with no interval arithmetic.
In the module's program this is the first kernel-checked signed Regge-convention deficit on an abstract four-tet star: strictly positive for one sign of $h$ and strictly negative for the other in the weak-field regime. It sits in the geometry layer that feeds hinge-aware Regge analysis; it does not itself invoke the T0-T8 forcing chain, but it supplies the local curvature sign control those continuum limits need on this mesh family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.