Termination of ordinary trigonometric comparisons

At nonzero rational arguments, sine, cosine, and arctangent are irrational. Their converging rational endpoints therefore exclude every rational boundary at some finite degree. Tangent uses a linear residual: its nonvanishing follows from tangent's irrationality and the absence of tangent poles at rational inputs. Exact zero-input values are handled by the comparison runtime before refinement.

theorem FloatLib.Numerics.Enclosure.exists_sin_separating (argument boundary : ℚ) (hnonzero : argument ≠ 0) : ∃ (n : ℕ), Comparison.Separates (sinReduced argument (2 ^ n)) boundary

Adaptive reduced sine enclosures eventually separate every rational boundary.

theorem FloatLib.Numerics.Enclosure.exists_cos_separating (argument boundary : ℚ) (hnonzero : argument ≠ 0) : ∃ (n : ℕ), Comparison.Separates (cosReduced argument (2 ^ n)) boundary

Adaptive reduced cosine enclosures eventually separate every rational boundary.

theorem FloatLib.Numerics.Enclosure.exists_atan_separating (argument boundary : ℚ) (hnonzero : argument ≠ 0) : ∃ (n : ℕ), Comparison.Separates (atan argument (2 ^ n)) boundary

Adaptive arctangent enclosures eventually separate every rational boundary.

theorem FloatLib.Numerics.Enclosure.contains_sinSubCos (argument boundary : ℚ) (degree : ℕ) : (sinSubCos argument boundary degree).Contains (Real.sin ↑argument - ↑boundary * Real.cos ↑argument)

The tangent residual enclosure contains its exact real linear combination.

theorem FloatLib.Numerics.Enclosure.tendsto_sinSubCos_lo (argument boundary : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(sinSubCos argument boundary n).lo) Filter.atTop (nhds (Real.sin ↑argument - ↑boundary * Real.cos ↑argument))

The lower endpoints of the tangent residual converge to the exact residual.

theorem FloatLib.Numerics.Enclosure.tendsto_sinSubCos_hi (argument boundary : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(sinSubCos argument boundary n).hi) Filter.atTop (nhds (Real.sin ↑argument - ↑boundary * Real.cos ↑argument))

The upper endpoints of the tangent residual converge to the exact residual.

theorem FloatLib.Numerics.Enclosure.sin_sub_rat_mul_cos_ne_zero (argument boundary : ℚ) (hnonzero : argument ≠ 0) : Real.sin ↑argument - ↑boundary * Real.cos ↑argument ≠ 0

A rational tangent boundary never makes the residual zero at a nonzero rational argument.

theorem FloatLib.Numerics.Enclosure.exists_sinSubCos_separating (argument boundary : ℚ) (hnonzero : argument ≠ 0) : ∃ (n : ℕ), Comparison.Separates (sinSubCos argument boundary (2 ^ n)) 0

The tangent residual comparison terminates without constructing a quotient enclosure.