arcsin_le_pi_div_two_mul
plain-language theorem explainer
On the nonnegative unit interval, arcsin is bounded above by the chord through the origin and (1, π/2): arcsin(x) ≤ (π/2) x. Used as the nonnegative half of the absolute chord bound that controls weak-field Regge deficits on the four-tet hinge star. Proof multiplies Mathlib's classical inequality (2/π)y ≤ sin y on [0, π/2] by π/2 after substituting y = arcsin x.
Claim. For every real $x$ with $0 \le x \le 1$, one has $\arcsin x \le (\pi/2)\, x$.
background
The ambient module builds signed Regge-convention deficit angles on an abstract four-tetrahedron hinge star: four congruent tets share an interior edge, with squared-edge data certified nondegenerate by the Cayley–Menger sign. On the kernel-checked slice the common dihedral cosine equals a deformation parameter $h$, and the star-local deficit collapses to
$$\mathrm{deficit}(h)=2\pi-4\arccos(h)=4\arcsin(h).$$
Thus any linear bound on $\arcsin$ immediately yields mesh-controlled bounds on the deficit in the weak-field regime $|h|\le 1$.
The classical comparison used here is Mathlib's chord inequality for sine: on $[0,\pi/2]$ one has $(2/\pi)y\le\sin y$. Combined with $\sin(\arcsin x)=x$ on the unit interval, it produces the stated linear majorant for $\arcsin$ itself.
proof idea
Set $y:=\arcsin x$. Nonnegativity of $x$ gives $y\ge 0$; the range of arcsin gives $y\le\pi/2$. Mathlib's mul_le_sin then supplies
$$(2/\pi),y\le\sin y.$$
Substitute $\sin y=x$ via sin_arcsin. Multiply both sides by the positive constant $\pi/2$ and cancel $(2/\pi)\cdot(\pi/2)=1$ by field_simp, obtaining $y\le(\pi/2)x$ as required.
why it matters
This is the nonnegative half of the absolute chord bound abs_arcsin_le_abs, which is the quantitative engine for weak-field deficit estimates on the four-tet star. Because the module identity $\mathrm{deficit}(h)=4\arcsin(h)$ is exact (no interval arithmetic, no native_decide), a pure comparison $\lvert\arcsin h\rvert\le(\pi/2)\lvert h\rvert$ converts immediately into
$$\lvert\mathrm{deficit}(h)\rvert\le 2\pi\lvert h\rvert$$
on the closed unit interval. That mesh-linear control is what lets the module certify that the signed deficit is strictly positive for one sign of the deformation parameter and strictly negative for the other, inside an explicit weak-field window. In the broader Recognition geometry stack this is scaffolding for hinge-local curvature signs before any global triangulation or Einstein-limit analysis is attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.