Proof contracts for configured logarithmic decoding

The runtime decoder exposes an exact rational through the common ExactDecoder interface. These lemmas connect that interface both to the logarithmic code's executable rational denotation and to its real-valued specification.

@[simp]

theorem FloatLib.Floats.ExecFloat.Logarithmic.Conversion.exactDecoder_run {radix : Numerics.Radix} (value : Logarithmic radix) : ExactDecoder.run value = Numerics.NumericalValue.finite value.toCode.toRat

The installed logarithmic source capability uses the executable exact rational decoder.

theorem FloatLib.Floats.ExecFloat.Logarithmic.Conversion.cast_toCode_toRat {radix : Numerics.Radix} (value : Logarithmic radix) : ↑value.toCode.toRat = value.toReal

Exact rational decoding agrees with the configured format's real semantics.