Correct rounding of pi

toReal_pi proves that Model.pi is the nearest-even rounding of Real.pi in every IEEE descriptor, and isFinite_pi that it is finite. The cached enclosure contains π * 2 ^ bits by halfPiLower_spec, so an accepted enclosure gives the rounding by toReal_eq_roundAt_of_roundScaled?_eq_some. The comparator fallback compares atan 1 = π / 4 exactly, and its result is finite because π < 3.15 lies below the overflow threshold of every IEEE descriptor: the smallest, ieee 2 1, has largest finite value 3 and threshold 3.5. isFinite_round_of_lt_overflow states that threshold argument for any exact comparator.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.isFinite_round_of_lt_overflow (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Bool) (compare : ℚ → Ordering) (target : ℝ) (hcompare : ∀ (candidate : ℚ), compare candidate = cmp target ↑candidate) (hbound : target < Flocq.bpow Numerics.binaryRadix (fmt.maxNormalExponent + 1) - Flocq.bpow Numerics.binaryRadix (fmt.maxNormalExponent - ↑fmt.fracWidth - 1)) : (round fmt sign compare).isFinite = true

An exact comparator for a target below the overflow threshold 2 ^ (maxNormal + 1) - 2 ^ (maxNormal - fracWidth - 1) gives a finite IEEE result.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.contains_piScaledEnclosure (bits : ℕ) : (piScaledEnclosure bits).Contains (Real.pi * 2 ^ bits)

The cached enclosure contains π * 2 ^ bits.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.pi_lt_overflowThreshold (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : Real.pi < Flocq.bpow Numerics.binaryRadix (fmt.maxNormalExponent + 1) - Flocq.bpow Numerics.binaryRadix (fmt.maxNormalExponent - ↑fmt.fracWidth - 1)

π lies below the overflow threshold of every IEEE descriptor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_pi (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : (pi fmt).isFinite = true

Model.pi is finite in every IEEE descriptor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_pi (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : (pi fmt).toReal = roundAt fmt Real.pi

Model.pi is the nearest-even rounding of Real.pi in every IEEE descriptor.