Agreement between policy and directed dyadic rounding

roundDyadicGeneral and roundDyadicWithRounding are independent executable algorithms. The first embeds a dyadic into the rational policy engine; 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; it is not merely an equality of real denotations.

The ordinary roundDyadic entry point dispatches recognized IEEE policies to the directed engine. Nearest-away, stochastic, saturating, and flush-to-zero policies remain specified by the general policy implementation.

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

General policy rounding under an explicit 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.