Terminating comparisons at rational multiples of pi

The exact-value classifiers remove all rational answers before refinement. Their completeness and endpoint convergence then separate every rational boundary. Tangent additionally excludes half-integer poles and compares a linear sine/cosine residual without dividing intervals.

theorem FloatLib.Numerics.Enclosure.exists_sinPi_separating (argument boundary : ℚ) (hnone : TrigonometricComparison.sinPiExact argument = none) : ∃ (n : ℕ), Comparison.Separates (sinPi argument (2 ^ n)) boundary

An unclassified pi-scaled sine eventually separates every rational boundary.

theorem FloatLib.Numerics.Enclosure.exists_cosPi_separating (argument boundary : ℚ) (hnone : TrigonometricComparison.cosPiExact argument = none) : ∃ (n : ℕ), Comparison.Separates (cosPi argument (2 ^ n)) boundary

An unclassified pi-scaled cosine eventually separates every rational boundary.

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

The tangent residual enclosure contains its exact real linear combination.

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

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

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

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

theorem FloatLib.Numerics.Enclosure.sinPi_sub_rat_mul_cosPi_ne_zero (argument boundary : ℚ) (hpole : Int.fract argument ≠ 1 / 2) (hnone : TrigonometricComparison.tanPiExact argument = none) : Real.sin (↑argument * Real.pi) - ↑boundary * Real.cos (↑argument * Real.pi) ≠ 0

Outside exact tangent values and poles, no rational boundary makes the residual vanish.

theorem FloatLib.Numerics.Enclosure.exists_sinPiSubCos_separating (argument boundary : ℚ) (hpole : Int.fract argument ≠ 1 / 2) (hnone : TrigonometricComparison.tanPiExact argument = none) : ∃ (n : ℕ), Comparison.Separates (sinPiSubCos argument boundary (2 ^ n)) 0

The pi-scaled tangent residual search terminates away from exact values and poles.