starDeficit_eq_arcsin
plain-language theorem explainer
On the one-parameter four-tetrahedron hinge star, the Regge deficit equals four times arcsin of the deformation parameter h. Anyone proving sign, oddness, flatness, or weak-field bounds for this star cites this closed form. The proof rewrites the arccos expression via the complementary-angle identity and simplifies.
Claim. For every real $h$, the star-local Regge deficit at the common hinge of the four congruent tetrahedra equals $4\arcsin(h)$.
background
The module studies an abstract four-tetrahedron hinge star: four congruent tets share an interior edge AB in a closed 4-cycle link, given by squared-edge data rather than an embedded triangulation. With the panel-locked slice $l=m=1$ and deformation $p(h)=(3/2)(1-h)$, the common dihedral cosine at AB is exactly the rational parameter $q=h$.
The star deficit is the Regge quantity $2\pi$ minus the sum of the four equal dihedral angles at AB. Each angle is computed by the repository's squared-edge dihedral formula. An upstream theorem already records the arccos form: the deficit equals $2\pi-4\arccos(h)$. The classical identity $\arccos h=\pi/2-\arcsin h$ then converts that expression into a pure arcsin formula, which is the content of the present result.
Geometrically, $h=0$ is the flat configuration ($p=3/2$, right dihedral angles, deficit zero). The sign of $h$ will later certify the sign of the deficit without interval arithmetic.
proof idea
One short rewrite chain. First apply the upstream equality that the star deficit is $2\pi-4\arccos(h)$. Then replace $\arccos$ by the Mathlib identity $\arccos h=\pi/2-\arcsin h$. The resulting expression $2\pi-4(\pi/2-\arcsin h)$ simplifies by ring arithmetic to $4\arcsin h$.
why it matters
This is the closed arcsin form advertised in the module design: deficit$(h)=4\arcsin(h)$. It is the algebraic bridge from the arccos definition of the star deficit to every signed and quantitative corollary in the file.
Downstream, the flatness theorem (deficit vanishes at $h=0$), the oddness theorem (deficit$(-h)=-\mathrm{deficit}(h)$), the signed-deficit contact certificate (sign of the deficit equals sign of $h$), and the weak-field bound $|\mathrm{deficit}(h)|\le 2\pi|h|$ all rewrite through this identity and then use elementary arcsin facts. Outside the module, the 4D recognition-mesh geometric deficit is defined to equal the star deficit and inherits the same arcsin formula in one line.
In the broader Recognition geometry stack this supplies the first kernel-checked signed Regge deficit on an abstract four-tet star, with explicit mesh-friendly bounds and no native decision procedures. It does not yet touch the forcing chain (T0–T8) or the J-cost; it is pure hinge geometry feeding later gravity/mesh analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.