sub_cube_le_sin
plain-language theorem explainer
For every real t ≥ 0, the cubic Taylor remainder yields t − t³/6 ≤ sin t with no smallness restriction on t. Cited by anyone proving global discrete-sine eigenvalue rates where the argument πk/N need not be small. The proof shows g(s) = sin s − s + s³/6 has nonnegative derivative (via the standard cosine inequality), hence is monotone, and g(t) ≥ g(0) = 0.
Claim. For every real number $t \ge 0$, one has $t - \frac{t^3}{6} \le \sin t$.
background
This module is the Phase 2a spectral-convergence toolkit for the QG campaign: quantitative eigenvalue limits that later curved-operator arguments consume. Mathlib already has a local cubic sine bound under $|t| \le 1$, but discrete sine eigenvalues involve arguments $\pi k/N$ that are not small for large wavenumber $k$, so a global bound is required.
The classical comparison used here is the cosine inequality $1 - s^2/2 \le \cos s$ (Mathlib Real.one_sub_sq_div_two_le_cos), which rearranges to a nonnegative derivative for the cubic remainder. The matching upper comparison $\sin t \le t$ for $t \ge 0$ is already Mathlib's Real.sin_le. Together they give a two-sided cubic Taylor control with no radius restriction.
proof idea
Introduce $g(x) = \sin x - x + x^3/6$. Establish pointwise HasDerivAt for $g$ with derivative $\cos s - 1 + s^2/2$, by subtracting the identity derivative from Real.hasDerivAt_sin and adding the scaled cubic derivative from hasDerivAt_pow.
Apply monotone_of_hasDerivAt_nonneg: the cosine inequality rearranges (via linarith) to show the derivative is nonnegative everywhere, so $g$ is monotone on $\mathbb{R}$. Evaluate $g(0) = 0$ by simp. Monotonicity at $t \ge 0$ then forces $g(t) \ge g(0)$, which rearranges by linarith to the claimed lower bound.
why it matters
Immediate parent is abs_sin_sub_le_cube, which packages this lower bound with Real.sin_le into the two-sided global estimate $|\sin t - t| \le t^3/6$ (no $|t| \le 1$ hypothesis). That absolute bound is the analytic engine of discrete_sine_eigenvalue_expansion: the sharp rate $|4N^2 \sin^2(\pi k/N) - (2\pi k)^2| \le ((2\pi k)^4/12)/N^2$ that upgrades the qualitative DiscreteLichnerowicz tendsto to an explicit $N^{-2}$ rate.
Phase 4 curved perturbation bounds and spectrum_gap_persistence consume that rate branch by branch. Closing Mathlib's smallness gap is essential when high lattice modes are present; without it the eigenvalue expansion would only cover low wavenumbers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.