starDeficit
plain-language theorem explainer
Star-local Regge deficit at the shared hinge of a four-tetrahedron star, as a real function of the deformation parameter h. It is 2π minus four equal dihedral angles computed from squared-edge star data. Downstream signed-deficit and weak-field theorems cite it as the explicit deficit family. The body is a one-line definition applying the repository dihedral-angle map on the star configuration.
Claim. For $h \in \mathbb{R}$, the star-local Regge deficit is $\delta(h) = 2\pi - 4\,\theta\bigl(a(h)\bigr)$, where $a(h)$ is the squared-edge 6-vector of the star tetrahedron with rim length $p(h)=\tfrac{3}{2}(1-h)$, and $\theta$ is the dihedral angle at hinge edge 0 obtained as $\arccos$ of the Cayley–Menger cosine on that data.
background
The module studies an abstract four-tet hinge star: four congruent tetrahedra around a common edge AB in a closed 4-cycle link, given only as squared-edge data (not an encoded triangulation). With hinge and leg lengths fixed at $l=m=1$, the rim length is the one-parameter family $p(h)=\tfrac{3}{2}(1-h)$. Flat closure is at $h=0$ ($p=3/2$), where the common hinge cosine vanishes and each dihedral angle is $\pi/2$.
The dihedral angle map takes squared edges and a hinge index to $\arccos$ of the Cayley–Menger cofactor cosine. Congruence forces all four incident angles equal, so the Regge deficit collapses to $2\pi$ minus four copies of that single angle. The module’s kernel-checked slice yields hinge cosine $q=h$ exactly, so the deficit is later rewritten as $2\pi-4\arccos(h)=4\arcsin(h)$ without interval arithmetic.
proof idea
Pure definition: evaluate the repository dihedral-angle function on the squared-edge star configuration built from rim length $p(h)$, at hinge index 0, multiply by four, and subtract from $2\pi$. No lemmas are applied at the definition site; subsequent theorems unfold this body and rewrite via the star cosine identity $q=h$.
why it matters
This is the explicit deficit family that makes the module’s signed Regge certificates possible. It feeds fourTet_deficit_eq (closed form $2\pi-4\arccos h$), starDeficit_eq_arcsin / fourTet_deficit_sign (sign of deficit equals sign of rational cosine $h$), fourTet_weak_pair (weak-field opposite-sign pair with exact antisymmetry), magnitude bounds, and the even-function obstruction even_cannot_match_starDeficit. The convention note records alignment with the standalone Regge deficit convention ($2\pi$ minus sum of incident dihedrals) without yet instantiating a full Triangulation3D. In the broader RS geometry stack this supplies the first kernel-checked signed hinge deficit on an abstract star, supporting continuum-bridge and ledger comparisons that need genuine sign, not absolute curvature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.