starDeficit_abs_le
plain-language theorem explainer
In the weak-field regime |h| ≤ 1, the absolute star-local Regge deficit on the four-tetrahedron hinge is at most 2π|h|. Anyone citing the signed four-tet deficit family or the weak-field pair certificate needs this magnitude control. The proof rewrites the deficit as 4 arcsin(h) and applies the chord bound |arcsin x| ≤ (π/2)|x| on the unit interval.
Claim. For every real $h$ with $|h| \le 1$, the absolute value of the star-local Regge deficit at deformation parameter $h$ satisfies $|\mathrm{deficit}(h)| \le 2\pi |h|$.
background
The module builds an abstract four-tetrahedron hinge star: four congruent tetrahedra around a common edge AB, given as squared-edge data (not an embedded triangulation). With hinge and leg lengths fixed at 1, the equatorial rim is deformed by $p(h)=(3/2)(1-h)$, so the common dihedral cosine equals $h$ on the nose.
The star-local deficit is $2\pi$ minus four equal dihedral angles at AB. On this slice it collapses to the closed form $4\arcsin(h)$, so the sign of the deficit tracks the sign of the rational cosine $h$ with no arccos evaluation. The only analytic input is the absolute chord bound $|\arcsin x|\le(\pi/2)|x|$ on the closed unit interval, proved earlier in the same module.
proof idea
Rewrite via the closed arcsin identity for the star deficit, then factor absolute values: $|4\arcsin h|=4|\arcsin h|$. Apply the private chord bound $|\arcsin h|\le(\pi/2)|h|$ under $|h|\le 1$. Simplify $|4|=4$ by norm_num and finish with linear arithmetic, since $4\cdot(\pi/2)|h|=2\pi|h|$.
why it matters
This is the weak-field magnitude estimate that feeds the weak-field signed pair certificate, which packages opposite-sign deficits at $\pm h^2$ with exact antisymmetry and explicit rational hinge cosines. Together they give the first kernel-checked signed Regge-convention deficits on an abstract four-tet star in the repository, with mesh bounds. In the Recognition geometry stack the result supplies controlled hinge curvature data for discrete gravity arguments; it does not yet bridge to a full Triangulation3D embedding or continuum Einstein equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.