Correctness of direct generic dyadic rounding

The executable integer implementation in RoundDyadicImpl.Runtime is extensionally equal to the logical Float.Model.UnpackedFloat.round specification used by ieeeRoundDyadic. The @[csimp] theorems install the direct implementation in compiled code while preserving the model-facing definitions in the type theory.

The IEEE proof covers signed zero, subnormal rounding, the minimum-normal transition, normalization carry, and overflow at arbitrary field widths. roundDyadicGeneral_eq_roundDyadic then relates the descriptor-aware algorithm to the public specification, including non-IEEE encoding policies.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofModel_finite_normalized_eq_ofFields (fmt : FloatFormat) (negative : Bool) (mantissa : ℕ) (exponent : ℤ) (hlow : pow2 fmt.fracWidth ≤ mantissa) (hhigh : mantissa < pow2 (fmt.fracWidth + 1)) (hmin : fmt.ieeeMinNormalExponent ≤ exponent) (hmax : exponent ≤ Int.ofNat fmt.ieeeMaxNormalExponent) : ofModel fmt (Float.Model.UnpackedFloat.finite (modelSign negative) mantissa (exponent - ↑fmt.fracWidth) ⋯) = ofFields fmt negative (exponent + Int.ofNat fmt.bias).toNat (mantissa - pow2 fmt.fracWidth)

Packing a normalized finite model value agrees with direct field construction.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ieeeRoundDyadic_eq_ieeeRoundDyadicImpl : ieeeRoundDyadic = ieeeRoundDyadicImpl

The direct integer dyadic rounder computes the same result as Lean's format-parameterized logical float model. The compiler uses this checked equality to replace the logical model at runtime.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicGeneral_eq_roundDyadic (fmt : FloatFormat) (d : Numerics.Dyadic) : roundDyadicGeneral fmt d = roundDyadic fmt d

The descriptor-general nearest-even dyadic algorithm agrees exactly with the public dyadic rounding specification, including signed zero and every packed exceptional result.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic_eq_roundDyadicImpl : roundDyadic = roundDyadicImpl

Compiler substitution preserves the complete-format dyadic rounding specification.