Static-byte exact conversion proofs

Exact conversion satisfies reduction equations for finite, infinite, and exceptional observations, and its installed exact decoder agrees with the public runtime function.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.run_finite {F : Type u} [Family F] (context : ExecFloat.Binary.Conversion.Context) (exact : Numerics.SignedRat) : run context (Numerics.NumericalValue.finite exact) = quantizeFinite context exact

Finite observations are handled by the shared exact rational binary quantizer.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.run_infinity {F : Type u} [Family F] (context : ExecFloat.Binary.Conversion.Context) (negative : Bool) : run context (Numerics.NumericalValue.infinity negative) = quantizeInfinity context negative

Infinity observations dispatch to the infinity quantizer.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.run_exceptional {F : Type u} [Family F] (context : ExecFloat.Binary.Conversion.Context) (exceptional : Numerics.ExceptionalValue) : run context (Numerics.NumericalValue.exceptional exceptional) = quantizeExceptional context exceptional

Exceptional observations dispatch to the exceptional-value quantizer.

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.implements_run {F : Type u} [Family F] : spec.Implements run

The static-byte converter inherits the shared nearest-value and complete-outcome clauses.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.exactDecoder_run {F : Type u} [Family F] (value : ExecFloat F) : ExecFloat.ExactDecoder.run value = decode value

The installed exact decoder is the public static-byte decoder.