Precision-grid proofs for P3109 projection

P3109 rounds to a descriptor-dependent binary grid before applying saturation. This module proves that the width-independent rounding kernel always produces either zero or a finite value that fits the descriptor precision and minimum quantum.

theorem FloatLib.Floats.Formats.P3109.Format.quantumExponent_lower (format : Format) (leading : ℤ) : format.minimumQuantumExponent ≤ max leading format.minimumNormalExponent - Int.ofNat format.precision + 1

Every descriptor-selected quantum is no smaller than the minimum encodable quantum.

def FloatLib.Floats.Formats.P3109.Format.FitsPrecisionGrid (format : Format) (value : Numerics.Dyadic) : Prop

Precision and minimum-quantum bounds for a dyadic, before finite-range saturation.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteToPrecision_fitsPrecisionGrid (format : Format) (mode : RoundingMode) (value : Numerics.Dyadic) : format.FitsPrecisionGrid (format.roundFiniteToPrecision mode value)

Precision rounding lands on the descriptor grid for every P3109 rounding mode.

The bound includes the carry significand 2^P, which the encoder advances to the next exponent row.