Correctness and termination of enclosure comparison

Containment proves the ordering at every successful search. Endpoint convergence proves that the search terminates whenever the target differs from the boundary. Irrationality is one convenient sufficient condition when the boundaries are rational.

theorem FloatLib.Numerics.Enclosure.Comparison.compare_eq_real (intervals : ℕ → RationalInterval) (boundary : ℚ) (terminates : ∃ (n : ℕ), Separates (intervals n) boundary) (x : ℝ) (contains : ∀ (n : ℕ), (intervals n).Contains x) : compare intervals boundary terminates = cmp x ↑boundary

Every accepted comparison agrees with the enclosed real value.

theorem FloatLib.Numerics.Enclosure.Comparison.exists_separating {intervals : ℕ → RationalInterval} {x : ℝ} (boundary : ℚ) (hne : x ≠ ↑boundary) (hlo : Filter.Tendsto (fun (n : ℕ) => ↑(intervals n).lo) Filter.atTop (nhds x)) (hhi : Filter.Tendsto (fun (n : ℕ) => ↑(intervals n).hi) Filter.atTop (nhds x)) : ∃ (n : ℕ), Separates (intervals n) boundary

Converging endpoints eventually exclude every boundary different from their limit.

theorem FloatLib.Numerics.Enclosure.Comparison.exists_separating_of_irrational {intervals : ℕ → RationalInterval} {x : ℝ} (hx : Irrational x) (boundary : ℚ) (hlo : Filter.Tendsto (fun (n : ℕ) => ↑(intervals n).lo) Filter.atTop (nhds x)) (hhi : Filter.Tendsto (fun (n : ℕ) => ↑(intervals n).hi) Filter.atTop (nhds x)) : ∃ (n : ℕ), Separates (intervals n) boundary

An irrational limit cannot equal a rational comparison boundary.