Every nonzero argument has an accepting window

For m > 0, m * 2 ^ e * 2/π is irrational because π is (irrational_pi), so it keeps a positive distance d from every integer. A reduction of it satisfies |fraction + η| ≥ d * 2 ^ scale with 0 ≤ η < error, so |fraction| > d * 2 ^ scale - error. The error of reduceWindow is 2 m for every window while 2 ^ scale doubles with each bit of window, so every window with 2 m * (2 ^ (bits + 1) + 1) < d * 2 ^ scale is accepted (exists_accepting_window). The attempt windows of reduce double, so enough fuel reaches an accepted reduction (exists_accepts_reduce).

The runtime bounds its attempts and checks the acceptance of the one it returns, so it needs neither theorem. They show that the bound on attempts is a resource limit: the method itself always succeeds.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.irrational_mul_two_div_pi {m : ℕ} (hm : 0 < m) (e : ℤ) : Irrational (↑m * 2 ^ e * (2 / Real.pi))

m * 2 ^ e * 2/π is irrational for m > 0.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.exists_accepting_window {m : ℕ} (hm : 0 < m) (e : ℤ) (bits : ℕ) : ∃ (start : ℕ), ∀ (window : ℕ), start ≤ window → QuarterTurns.accepts bits (reduceWindow m e window) = true

For m > 0, every wide enough window reduces m * 2 ^ e with bits relative bits: QuarterTurns.accepts bits holds for all windows from some start on.

theorem FloatLib.Numerics.Enclosure.ArgumentReduction.exists_accepts_reduce {m : ℕ} (hm : 0 < m) (e : ℤ) (p bits : ℕ) : ∃ (fuel : ℕ), QuarterTurns.accepts bits (reduce m e p bits fuel) = true

For m > 0, enough fuel makes reduce return an accepted reduction.