Shared exponent selection for concrete OCP MX blocks

The selected exponent is the binade exponent of the largest input magnitude minus the largest element power-of-two exponent. E8M0 bounds every scale that reaches element quantization. The binade theorem reuses the format-independent proof of the executable rational logarithm.

theorem FloatLib.Floats.Formats.OCP.MX.E8M0.exponent?_bounds {scale : E8M0} {exponent : ℤ} (h : scale.exponent? = some exponent) : -127 ≤ exponent ∧ exponent ≤ 127

Every finite E8M0 scale has a bounded exponent.

@[simp]

theorem FloatLib.Floats.Formats.OCP.MX.E8M0.exponent?_ofExponentSaturating (exponent : ℤ) : (ofExponentSaturating exponent).exponent? = some (max (-127) (min 127 exponent))

Saturating E8M0 encoding decodes to the clamped mathematical exponent.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.maxMagnitude_nonneg (input : Vector Numerics.SignedRat 32) : 0 ≤ maxMagnitude input

The largest input magnitude is nonnegative, including the all-zero block.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.abs_le_maxMagnitude (input : Vector Numerics.SignedRat 32) (lane : Fin 32) : |input[↑lane].value| ≤ maxMagnitude input

Every lane is bounded by the magnitude used for standard scale selection.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.requestedExponent_bounds (profile : Profile) (input : Vector Numerics.SignedRat 32) (hnonzero : maxMagnitude input ≠ 0) : 2 ^ (requestedExponent profile input + profile.maxPowerExponent) ≤ ↑(maxMagnitude input) ∧ ↑(maxMagnitude input) < 2 ^ (requestedExponent profile input + profile.maxPowerExponent + 1)

For a nonzero input block, the requested scale positions the largest magnitude between the element's largest positive power of two and twice that value, before E8M0 range handling.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.selectScale_exponent?_of_overflow (profile : Profile) (input : Vector Numerics.SignedRat 32) (h : 127 < requestedExponent profile input) : (selectScale profile input).exponent? = none

Out-of-range upper scales propagate a block NaN instead of constructing an invalid exponent.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.selectScale_exponent?_of_le (profile : Profile) (input : Vector Numerics.SignedRat 32) (h : requestedExponent profile input ≤ 127) : (selectScale profile input).exponent? = some (max (-127) (requestedExponent profile input))

Finite scale selection clamps only at the lower E8M0 boundary.