Rounded-real meaning of Lean accuracy certificates

Lean's unpacked-float model represents a positive real by a truncated natural mantissa, an exponent, and an Accuracy certificate. This module proves that roundWithAccuracy rounds that real exactly as the independent Flocq-style roundAt model whenever normalization only shifts right and the packed output remains finite. Agreement with roundAt requires a conventional IEEE descriptor. This bridge is used by square root and other non-dyadic kernels.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cexp_accuracy_mul_bpow_eq_targetExponent (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (accuracy : Float.Model.UnpackedFloat.Accuracy) (value : ℝ) (hfmt : fmt.isIEEE = true) (hmantissa : mantissa ≠ 0) (haccuracy : accuracyRepresents mantissa accuracy value) : Flocq.cexp Numerics.binaryRadix (fexpOf fmt) (value * Flocq.bpow Numerics.binaryRadix exponent) = fmt.toModel.targetExponent (Float.Model.totalExponent mantissa exponent)

The model and rounded-real semantics choose the same exponent for a valid certificate.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaledMantissa_accuracy_mul_bpow (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (accuracy : Float.Model.UnpackedFloat.Accuracy) (value : ℝ) (hfmt : fmt.isIEEE = true) (hmantissa : mantissa ≠ 0) (haccuracy : accuracyRepresents mantissa accuracy value) : Flocq.scaledMantissa Numerics.binaryRadix (fexpOf fmt) (value * Flocq.bpow Numerics.binaryRadix exponent) = value * Flocq.bpow Numerics.binaryRadix (exponent - fmt.toModel.targetExponent (Float.Model.totalExponent mantissa exponent))

The certificate value at the model exponent is the canonical scaled mantissa.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.shiftToTargetExponent_eq_of_le_targetExponent (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (accuracy : Float.Model.UnpackedFloat.Accuracy) (hle : exponent ≤ fmt.toModel.targetExponent (Float.Model.totalExponent mantissa exponent)) : Float.Model.UnpackedFloat.shiftToTargetExponent fmt.toModel mantissa exponent accuracy = (Float.Model.UnpackedFloat.ExtendedMantissa.ofMantissaAndAccuracy mantissa accuracy >>> (fmt.toModel.targetExponent (Float.Model.totalExponent mantissa exponent) - exponent).toNat, fmt.toModel.targetExponent (Float.Model.totalExponent mantissa exponent))

When no left shift is needed, the first stage of roundWithAccuracy shifts the extended mantissa right to the target exponent and reports that exponent unchanged.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundedMantissa_shiftToTargetExponent_eq_nearestEven (fmt : FloatFormat) (mantissa : ℕ) (exponent : ℤ) (accuracy : Float.Model.UnpackedFloat.Accuracy) (value : ℝ) (haccuracy : accuracyRepresents mantissa accuracy value) (hle : exponent ≤ fmt.toModel.targetExponent (Float.Model.totalExponent mantissa exponent)) : Int.ofNat (Float.Model.UnpackedFloat.shiftToTargetExponent fmt.toModel mantissa exponent accuracy).1.roundedMantissa = Flocq.nearestEven (value * Flocq.bpow Numerics.binaryRadix (exponent - fmt.toModel.targetExponent (Float.Model.totalExponent mantissa exponent)))

When no left shift is needed, the rounded mantissa produced by the first stage of roundWithAccuracy is the nearest-even integer of the represented real scaled to the target exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_ofModel_roundWithAccuracy_eq_roundAt (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (exponent : ℤ) (accuracy : Float.Model.UnpackedFloat.Accuracy) (value : ℝ) (hmantissa : mantissa ≠ 0) (haccuracy : accuracyRepresents mantissa accuracy value) (hle : exponent ≤ fmt.toModel.targetExponent (Float.Model.totalExponent mantissa exponent)) (hfinite : (ofModel fmt (Float.Model.UnpackedFloat.roundWithAccuracy fmt.toModel sign mantissa exponent accuracy)).isFinite = true) : (ofModel fmt (Float.Model.UnpackedFloat.roundWithAccuracy fmt.toModel sign mantissa exponent accuracy)).toReal = roundAt fmt ((if modelSignBit sign = true then -1 else 1) * (value * Flocq.bpow Numerics.binaryRadix exponent))

Lean's signed roundWithAccuracy result has the same real value as independent nearest-even rounding of the represented signed real. The exponent premise is the documented precondition of roundWithAccuracy: normalization may discard low bits, but must not require a preliminary left shift. The finiteness premise excludes IEEE overflow, which has no value in Real.