Scaled-dyadic lemmas for the policy agreement proofs

The general policy engine roundRatGeneralOfDenNeZero receives an exact dyadic mantissa * 2^exponent as the scaled rational scaleByPowerOfTwo mantissa 1 exponent. The lemmas here carry that representation through the engine's two quotient sites, the subnormal alignment and the normal significand, and identify each quotient with a shift primitive of the dyadic rounders: nearest-even with roundMantissaAtExponentEven, floor and ceiling with roundMantissaAtExponentDown and roundMantissaAtExponentUp.

roundRatGeneralOfDenNeZero_nearest_dyadic_eq and roundRatGeneralOfDenNeZero_directed_dyadic_eq compare the engine with the nearest-even and the directed dyadic packers. Rounding.Policy.Agreement uses them for nearest-even rounding and the four directed modes, and Rounding.Policy.NearestAwayAgreement for nearest-away rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundQuot_nearest_eq_roundQuotientEven (sign : Bool) (entropy numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : roundQuot Numerics.RoundingMode.nearest sign entropy numerator denominator = Numerics.roundQuotientEven numerator denominator

The policy nearest-even quotient is the shared nearest-even quotient primitive.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundQuot_towardZero_eq_roundQuotDirected (sign : Bool) (entropy numerator denominator : ℕ) : roundQuot Numerics.RoundingMode.towardZero sign entropy numerator denominator = roundQuotDirected false numerator denominator

Policy truncation is the lower directed quotient primitive.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundQuot_up_eq_roundQuotDirected (sign : Bool) (entropy numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : roundQuot Numerics.RoundingMode.up sign entropy numerator denominator = roundQuotDirected (!sign) numerator denominator

Positive-direction policy rounding selects floor or ceiling from the encoded sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundQuot_down_eq_roundQuotDirected (sign : Bool) (entropy numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : roundQuot Numerics.RoundingMode.down sign entropy numerator denominator = roundQuotDirected sign numerator denominator

Negative-direction policy rounding selects floor or ceiling from the encoded sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundQuot_away_eq_roundQuotDirected (sign : Bool) (entropy numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : roundQuot Numerics.RoundingMode.away sign entropy numerator denominator = roundQuotDirected true numerator denominator

Away-from-zero policy rounding is the upper directed quotient primitive.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.floorLog2_scaleByPowerOfTwo_den_one (mantissa : ℕ) (exponent : ℤ) (hmantissa : mantissa ≠ 0) : have scaled := Numerics.RationalBinary.scaleByPowerOfTwo mantissa 1 exponent; Numerics.RationalBinary.floorLog2 scaled.1 scaled.2 = Int.ofNat mantissa.log2 + exponent

Absorbing a dyadic exponent into a quotient adds that exponent to its leading bit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.exponent_add_subnormalAlign (fmt : FloatFormat) (exponent : ℤ) : exponent + Int.ofNat (fmt.exponentBias + fmt.fracWidth - 1) = exponent - fmt.minSubnormalExponent

The policy engine's subnormal shift is the distance to the least-subnormal exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundRatGeneralOfDenNeZero_nearest_dyadic_eq (fmt : FloatFormat) (sign : Bool) (entropy mantissa : ℕ) (exponent : ℤ) : let scaled := Numerics.RationalBinary.scaleByPowerOfTwo mantissa 1 exponent; roundRatGeneralOfDenNeZero fmt Numerics.QuantizationPolicy.nearest entropy sign scaled.1 scaled.2 ⋯ = Model.roundDyadicGeneral fmt { negative := sign, significand := mantissa, exponent := exponent }

The independent rational policy core and descriptor-general dyadic rounder agree under nearest-even rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundRatGeneralOfDenNeZero_directed_dyadic_eq (fmt : FloatFormat) (rounding : Numerics.RoundingMode) (roundUp sign : Bool) (entropy mantissa : ℕ) (exponent : ℤ) (hquot : ∀ (numerator denominator : ℕ), denominator ≠ 0 → roundQuot rounding sign entropy numerator denominator = roundQuotDirected roundUp numerator denominator) (hoverflow : overflowRoundsMagnitudeUp rounding sign = roundUp) (htiny : tinyRoundsMagnitudeUp? rounding sign = some roundUp) : let scaled := Numerics.RationalBinary.scaleByPowerOfTwo mantissa 1 exponent; roundRatGeneralOfDenNeZero fmt { rounding := rounding } entropy sign scaled.1 scaled.2 ⋯ = roundRatMagnitudeDirectedScaled fmt roundUp sign mantissa 1 exponent

For a directed mode, the rational policy core applied to an exact dyadic is the shared directed rational packer. The two sides compute their quotients and branch on their own but share the packers packRoundedSubnormal and packRoundedNormal. The proof identifies their exact binary scalings before comparing branches.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundRatMagnitudeDirectedScaled_dyadic_eq (fmt : FloatFormat) (roundUp sign : Bool) (mantissa : ℕ) (exponent : ℤ) : roundRatMagnitudeDirectedScaled fmt roundUp sign mantissa 1 exponent = if mantissa = 0 then zero fmt sign else if roundUp = true then roundDyadicMagnitudeUp fmt sign mantissa exponent else roundDyadicMagnitudeDown fmt sign mantissa exponent

The rational directed packer specializes to the corresponding dyadic magnitude packer when the denominator is one.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Policy.roundDyadicGeneral_eq_roundRatGeneralOfDenNeZero (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) (value : Numerics.Dyadic) : roundDyadicGeneral fmt policy entropy value = let scaled := Numerics.RationalBinary.scaleByPowerOfTwo value.significand 1 value.exponent; roundRatGeneralOfDenNeZero fmt policy entropy value.negative scaled.1 scaled.2 ⋯

View the dyadic policy entry point as one exact rational scaling.

The runtime definition branches on the sign of the exponent to avoid constructing an unnecessary intermediate pair. This theorem gives proofs one uniform representation of that same computation.