Basic policy-rounding facts

This lightweight module contains the facts needed by arithmetic and conversion proofs: deterministic nearest-even behavior, flush-to-zero behavior, IEEE dispatch, and overflow policy equations.

The independent proof that the general rational policy engine agrees with the directed dyadic engine lives in Rounding.Policy.Agreement. Keeping that larger proof separate prevents ordinary finite arithmetic and conversion modules from inheriting its directed-semantics dependency graph.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundQuot_nearestEven_eq_zero (sign : Bool) (entropy num den : ℕ) : roundQuot Numerics.RoundingMode.nearestEven sign entropy num den = roundQuot Numerics.RoundingMode.nearestEven sign 0 num den

Nearest-even quotient rounding does not inspect the entropy source.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundDyadic_nearestEven_eq_zero (fmt : FloatFormat) (entropy : ℕ) (value : Numerics.Dyadic) : roundDyadic fmt Numerics.QuantizationPolicy.nearestEven entropy value = roundDyadic fmt Numerics.QuantizationPolicy.nearestEven 0 value

Nearest-even dyadic quantization is independent of the entropy argument.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundDyadicGeneral_nearestEven_eq_zero (fmt : FloatFormat) (entropy : ℕ) (value : Numerics.Dyadic) : roundDyadicGeneral fmt Numerics.QuantizationPolicy.nearestEven entropy value = roundDyadicGeneral fmt Numerics.QuantizationPolicy.nearestEven 0 value

Nearest-even general quantization is independent of the entropy argument.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.applyUnderflow_flush_of_subnormal (fmt : FloatFormat) (x : Model fmt) (hx : x.isSubnormal = true) : applyUnderflow fmt Numerics.UnderflowMode.flushToZero x = zero fmt x.signBit

Flushing a subnormal result produces the format's corresponding zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.applyUnderflow_flush_of_not_subnormal (fmt : FloatFormat) (x : Model fmt) (hx : x.isSubnormal = false) : applyUnderflow fmt Numerics.UnderflowMode.flushToZero x = x

Flush-to-zero leaves every non-subnormal encoding unchanged.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundRat_nearestEven_eq_execFloat (fmt : FloatFormat) (entropy : ℕ) (sign : Bool) (num den : ℕ) (hden : den ≠ 0) : roundRat fmt Numerics.QuantizationPolicy.nearestEven entropy sign num den = some (Model.roundRat fmt sign num den)

Default rational quantization is the canonical format-parameterized nearest-even rounder.

The entropy argument is irrelevant because nearest-even rounding is deterministic.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundDyadic_nearestEven_eq_execFloat (fmt : FloatFormat) (entropy : ℕ) (value : Numerics.Dyadic) : roundDyadic fmt Numerics.QuantizationPolicy.nearestEven entropy value = Model.roundDyadic fmt value

Default dyadic quantization is the canonical format-parameterized nearest-even rounder.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.ieeeRoundingMode?_toRoundingMode (mode : IEEERoundingMode) : ieeeRoundingMode? mode.toRoundingMode = some mode

Embedding an IEEE direction into the policy vocabulary and back is the identity.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.policyIEEERoundingMode?_toRoundingMode (mode : IEEERoundingMode) : policyIEEERoundingMode? { rounding := mode.toRoundingMode } = some mode

A native-overflow, gradual-underflow policy built from an IEEE direction names that direction.

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

Each embedded IEEERoundingMode dispatches to the directed engine.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowResult_native_eq_directedOverflow (fmt : FloatFormat) (rounding : Numerics.RoundingMode) (sign : Bool) : overflowResult fmt Numerics.OverflowMode.native rounding sign = directedOverflow fmt sign (overflowRoundsMagnitudeUp rounding sign)

Native policy overflow is the shared directed overflow rule.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowResult_native_nearestEven (fmt : FloatFormat) (sign : Bool) : overflowResult fmt Numerics.OverflowMode.native Numerics.RoundingMode.nearestEven sign = nativeOverflow fmt sign

Nearest rounding overflows to the format's native overflow value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowResult_native_towardZero (fmt : FloatFormat) (sign : Bool) : overflowResult fmt Numerics.OverflowMode.native Numerics.RoundingMode.towardZero sign = maxFinite fmt sign

Toward-zero rounding saturates to the largest finite magnitude with the requested sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowResult_native_towardPositive (fmt : FloatFormat) (sign : Bool) : overflowResult fmt Numerics.OverflowMode.native Numerics.RoundingMode.towardPositive sign = if sign = true then maxFinite fmt true else nativeOverflow fmt false

Positive-direction rounding selects native positive overflow and saturates negative overflow.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowResult_native_towardNegative (fmt : FloatFormat) (sign : Bool) : overflowResult fmt Numerics.OverflowMode.native Numerics.RoundingMode.towardNegative sign = if sign = true then nativeOverflow fmt true else maxFinite fmt false

Negative-direction rounding selects native negative overflow and saturates positive overflow.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.overflowResult_saturate (fmt : FloatFormat) (rounding : Numerics.RoundingMode) (sign : Bool) : overflowResult fmt Numerics.OverflowMode.saturate rounding sign = maxFinite fmt sign

Saturating overflow ignores the rounding direction.