abs_sin_sub_le_cube
plain-language theorem explainer
For every nonnegative real t, the sine function stays within t cubed over six of the identity: |sin t - t| ≤ t³/6. Analysts cite this as the global cubic Taylor remainder for sine without a small-angle hypothesis. The proof sandwiches sin t between t - t³/6 and t, then rewrites the absolute value as a two-sided linear inequality.
Claim. For every real number $t \geq 0$, $|\sin t - t| \leq t^3/6$.
background
This module is the Phase 2a spectral-convergence toolkit for the quantum-gravity campaign: reusable, axiom-clean analysis lemmas that upgrade qualitative eigenvalue limits to explicit rates. The discrete Lichnerowicz (flat TT) spectrum on a lattice of resolution $N$ involves factors $\sin(\pi k/N)$; the continuum target is the continuum wavenumber squared $(2\pi k)^2$. Controlling the difference requires a cubic bound on $\sin x - x$ that holds for all $x \geq 0$, not merely $|x| \leq 1$.
Mathlib supplies Real.sin_le (sine lies below the identity on the nonnegative reals) and the sibling lemma sub_cube_le_sin (the cubic lower envelope $t - t^3/6 \leq \sin t$), itself obtained from the cosine inequality Real.one_sub_sq_div_two_le_cos by a monotonicity argument. Mathlib's Real.sin_bound only covers the unit interval; the eigenvalue expansion needs the unrestricted form because $\pi k/N$ is not small for large wavenumber $k$.
proof idea
Three elementary facts are assembled. First, Real.sin_le gives $\sin t \leq t$ for $t \geq 0$. Second, the sibling sub_cube_le_sin gives the matching lower bound $t - t^3/6 \leq \sin t$. Third, positivity of $t^3/6$ is immediate. Rewriting the goal as the two-sided inequality $-t^3/6 \leq \sin t - t \leq t^3/6$ via abs_le, both sides follow by linarith from the three facts.
why it matters
The sole direct consumer is discrete_sine_eigenvalue_expansion, the sharp quantitative flat TT eigenvalue expansion
$|4N^2 \sin^2(\pi k/N) - (2\pi k)^2| \leq ((2\pi k)^4/12)/N^2$.
That derivation factors the error as $4N^2(\sin x - x)(\sin x + x)$ with $x = \pi k/N$, feeds in this cubic bound together with $|\sin x + x| \leq 2x$, and obtains the explicit constant $C(k) = (2\pi k)^4/12$. Phase 4 curved perturbation bounds consume that constant; the qualitative DiscreteLichnerowicz.discreteEigenvalue_tendsto is thereby upgraded to a rate that eigenvalue_limit_of_uniform_bound can squeeze to a limit. Within the broader Recognition gravity stack this is pure analysis scaffolding: it does not invoke the J-cost, the forcing chain, or the eight-tick octave, but it is the rate lemma that lets discrete spectral data converge cleanly enough for continuum identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.