Agreement between policy and directed dyadic rounding

roundDyadicGeneral and Internal.Directed.roundDyadic are independent executable algorithms. The first embeds a dyadic into the rational policy engine, and the second uses dedicated shift-based dyadic packers. This file proves that their complete packed results agree for each IEEERoundingMode when overflow is native and underflow is gradual. The proof includes signed zero, subnormal carry, custom exponent bias, finite-only encodings, and native overflow words, so it is more than an equality of real denotations.

The ordinary roundDyadic entry point dispatches these policies to the directed engine, so the agreement says that the dispatch does not change any result. Stochastic, saturating, and flush-to-zero policies are specified by the general policy implementation. The scaled-dyadic lemmas behind the proof are in Rounding.Policy.ScaledDyadic, and the nearest-away case is Rounding.Policy.NearestAwayAgreement.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundDyadicGeneral_toRoundingMode (fmt : FloatFormat) (mode : IEEERoundingMode) (entropy : ℕ) (value : Numerics.Dyadic) : roundDyadicGeneral fmt { rounding := mode.toRoundingMode } entropy value = Internal.Directed.roundDyadic fmt mode value

General policy rounding under an IEEE direction, native overflow, and gradual underflow is the directed rounder's complete packed result.

The entropy argument is irrelevant because every IEEERoundingMode is deterministic.