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

IEEE32Exec.Trig.sinCosTaylorSmall uses a reduced-input Taylor kernel (degree 13/12). For many proofs we only need some analytic bound saying the Taylor approximation is close on |x| ≤ 1.

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

• Real.sin_bound: |sin x - (x - x^3/6)| ≤ |x|^4 * (5/96) for |x| ≤ 1,
• Real.cos_bound: |cos x - (1 - x^2/2)| ≤ |x|^4 * (5/96) for |x| ≤ 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| ^ 4 * (5 / 96)

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