Real meaning of Lean accuracy certificates

Lean's logical floating-point model carries an Accuracy value alongside a truncated natural mantissa. This module states its intended real-number meaning, proves that right shifts preserve that meaning, and connects its nearest-even choice to the independent Flocq-style integer rounder.

def FloatLib.Floats.Formats.BinaryInterchange.Model.accuracyRepresents (mantissa : ℕ) (accuracy : Float.Model.UnpackedFloat.Accuracy) (value : ℝ) : Prop

accuracyRepresents mantissa accuracy value states that mantissa is the integer truncation of the nonnegative real value and that accuracy locates the discarded part relative to one half.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.accuracyRepresents_bounds {mantissa : ℕ} {accuracy : Float.Model.UnpackedFloat.Accuracy} {value : ℝ} (h : accuracyRepresents mantissa accuracy value) : ↑mantissa ≤ value ∧ value < ↑mantissa + 1

Every represented value lies in the unit interval beginning at its truncated mantissa.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.magnitude_of_accuracyRepresents {mantissa : ℕ} {accuracy : Float.Model.UnpackedFloat.Accuracy} {value : ℝ} (hmantissa : mantissa ≠ 0) (h : accuracyRepresents mantissa accuracy value) : Flocq.magnitude Numerics.binaryRadix value = Int.ofNat mantissa.log2 + 1

A nonzero truncated mantissa determines the binary magnitude of every real value represented by its accuracy certificate.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.accuracyRepresents_shiftRightOne (em : Float.Model.UnpackedFloat.ExtendedMantissa) (value : ℝ) (h : accuracyRepresents em.mantissa em.accuracy value) : accuracyRepresents em.shiftRightOne.mantissa em.shiftRightOne.accuracy (value / 2)

One model right shift preserves the accuracy certificate after dividing the represented real by two.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.accuracyRepresents_shift (em : Float.Model.UnpackedFloat.ExtendedMantissa) (value : ℝ) (shift : ℕ) (h : accuracyRepresents em.mantissa em.accuracy value) : accuracyRepresents (em >>> shift).mantissa (em >>> shift).accuracy (value / 2 ^ shift)

Repeated model right shifts preserve the certificate at the correspondingly divided scale.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToNearestEven_eq_nearestEven (mantissa : ℕ) (accuracy : Float.Model.UnpackedFloat.Accuracy) (value : ℝ) (h : accuracyRepresents mantissa accuracy value) : Int.ofNat (Float.Model.UnpackedFloat.Accuracy.roundToNearestEven mantissa accuracy) = Flocq.nearestEven value

A valid accuracy certificate makes Lean's and the real model's nearest-even choices equal.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundedMantissa_eq_nearestEven (mantissa : ℕ) (accuracy : Float.Model.UnpackedFloat.Accuracy) (value : ℝ) (shift : ℕ) (h : accuracyRepresents mantissa accuracy value) : Int.ofNat (Float.Model.UnpackedFloat.ExtendedMantissa.ofMantissaAndAccuracy mantissa accuracy >>> shift).roundedMantissa = Flocq.nearestEven (value / 2 ^ shift)

After any model right shift, rounding the resulting extended mantissa agrees with independent nearest-even rounding of the represented real at the shifted scale.