abs_arcsin_le_abs
plain-language theorem explainer
Absolute chord bound: for every real x with |x| ≤ 1, |arcsin x| ≤ (π/2)|x|. Cited by anyone controlling the weak-field size of the signed four-tet star deficit, which equals 4 arcsin(h). Proof is a two-case sign split that reduces to the nonnegative chord bound via oddness of arcsin.
Claim. For every real number $x$ with $|x| \le 1$, $|\arcsin x| \le \frac{\pi}{2}\,|x|$.
background
The module builds signed Regge-convention deficit angles on an abstract four-tetrahedron hinge star: four congruent tets around a common hinge, certified nondegenerate by Cayley–Menger (cm3 > 0). On the kernel-checked slice l = m = 1 the deformation p(h) = (3/2)(1 − h) forces the common dihedral cosine to equal h, so the star deficit collapses to deficit(h) = 2π − 4 arccos(h) = 4 arcsin(h). Sign of the deficit is then the sign of the rational parameter h; magnitude control needs a chord bound on arcsin.
The nonnegative half of that bound is already proved as the sibling lemma: arcsin(x) ≤ (π/2)x for 0 ≤ x ≤ 1, obtained from the classical inequality (2/π)y ≤ sin y on [0, π/2]. The present statement extends that half-line bound to the full closed unit interval by absolute values. Upstream, deficit itself is the standard hinge quantity 2π − Σ θ (DihedralAngle / Schläfli).
proof idea
Tactic proof by cases on the sign of x.
If x ≥ 0, drop both absolute values (arcsin is nonnegative on [0,1]) and apply the sibling nonnegative chord bound arcsin_le_pi_div_two_mul.
If x < 0, rewrite |x| = −x and |arcsin x| = −arcsin x, then use arcsin(−x) = −arcsin x to reduce to arcsin_le_pi_div_two_mul at −x (which lies in [0,1]). The only arithmetic is a short linarith discharging −x ≤ 1 from |x| ≤ 1.
why it matters
This is the absolute-value bridge from the nonnegative arcsin chord bound to the weak-field magnitude theorem starDeficit_abs_le: |deficit(h)| ≤ 2π|h| whenever |h| ≤ 1. That parent rewrites starDeficit as 4 arcsin(h), multiplies through by 4, and applies the present bound; the factor 2π is exactly 4 · (π/2).
In the Recognition geometry stack this closes the first kernel-checked magnitude estimate for a signed Regge deficit on an abstract four-tet star, complementary to the sign certification (sign(deficit) = sign(h)) already obtained without evaluating arccos. It does not itself invoke the forcing chain T0–T8, but it supplies the analytic control needed wherever discrete curvature deficits feed continuum or weak-field limits in the geometry layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.