Simple Taylor remainder bounds for Real.sin / Real.cos

IEEE32Exec.Trig.sinCosTaylorSmall uses a reduced-input Taylor kernel (degree 13/12). The theorems below are coarse analytic facts about separate degree-three/two baselines; they are not an accuracy contract for the executable kernel. For many proofs these baseline bounds are still useful on $|x|\le 1$.

Mathlib provides clean, reusable bounds for the first nontrivial truncations:

• Real.sin_bound: $|\sin x-(x-x^3/6)|\le |x|^5/100$ for $|x|\le 1$;
• Real.cos_bound: $|\cos x-(1-x^2/2)|\le |x|^4(5/96)$ for $|x|\le 1$.

These are coarse but robust and are often sufficient as a local ingredient in larger numerical proofs. Tighter bounds for higher-degree truncations can be added later if needed.

noncomputable def TorchLean.Floats.IEEE754.IEEE32Exec.cosTaylor2 (x : ℝ) : ℝ

Quadratic Taylor approximation $1-x^2/2$ used as a baseline for cos.

noncomputable def TorchLean.Floats.IEEE754.IEEE32Exec.sinTaylor2 (x : ℝ) : ℝ

Cubic Taylor approximation $x-x^3/6$ used as a baseline for sin.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.abs_sin_sub_sinTaylor2_le (x : ℝ) (hx : |x| ≤ 1) : |Real.sin x - sinTaylor2 x| ≤ |x| ^ 5 / 100

theorem TorchLean.Floats.IEEE754.IEEE32Exec.abs_cos_sub_cosTaylor2_le (x : ℝ) (hx : |x| ≤ 1) : |Real.cos x - cosTaylor2 x| ≤ |x| ^ 4 * (5 / 96)