Eventual acceptance of converging posit enclosures

Every comparison in posit rounding has a rational boundary. Consequently the rounded code is locally constant at an irrational target, and converging rational endpoints eventually agree. The result separates two mathematical obligations: the enclosure algorithm converges, and its target avoids the exact boundaries. A function-specific irrationality theorem or exact-case handler is still needed before this gives a total elementary operation.

theorem FloatLib.Floats.Formats.Posit.Model.Enclosure.eventually_lowerCode_eq (format : Format) {x : ℝ} (hx : Irrational x) : ∀ᶠ (y : ℝ) in nhds x, RealRounding.lowerCode format y = RealRounding.lowerCode format x

The finite lower-code search is locally constant at every irrational target.

theorem FloatLib.Floats.Formats.Posit.Model.Enclosure.eventually_roundPositiveCode_eq (format : Format) {x : ℝ} (hx : Irrational x) : ∀ᶠ (y : ℝ) in nhds x, RealRounding.roundPositiveCode format y = RealRounding.roundPositiveCode format x

Standard posit rounding is locally constant at every irrational real target.

theorem FloatLib.Floats.Formats.Posit.Model.Enclosure.eventually_roundPositive?_eq_some (format : Format) {intervals : ℕ → Numerics.RationalInterval} {x : ℝ} (hx : Irrational x) (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 : ℕ) in Filter.atTop, roundPositive? format (intervals n) = some (RealRounding.roundPositive format x)

Converging rational endpoints eventually certify the posit rounding of an irrational target.

Containment is not required for this eventual statement: convergence puts both endpoints in a neighborhood on which rounding is constant. Containment separately certifies every accepted result, including any accepted before that neighborhood is reached.

theorem FloatLib.Floats.Formats.Posit.Model.Enclosure.eventually_roundPositive?_exp (format : Format) (x : ℚ) (hx : Irrational (Real.exp ↑x)) : ∀ᶠ (degree : ℕ) in Filter.atTop, roundPositive? format (Numerics.Enclosure.exp x degree) = some (RealRounding.roundPositive format (Real.exp ↑x))

An irrational exponential target is eventually resolved by the rational Taylor enclosures.