Correctness of configured exact logarithmic operations

Wrapping is an equivalence with the complete code, zero denotes real zero, and multiplication agrees exactly with multiplication of decoded real values.

@[simp]

theorem FloatLib.Floats.ExecFloat.Logarithmic.toCode_ofCode {radix : Numerics.Radix} (code : Formats.Logarithmic.Code radix) : (ofCode code).toCode = code

Unwrapping a freshly wrapped logarithmic code returns the original code.

@[simp]

theorem FloatLib.Floats.ExecFloat.Logarithmic.ofCode_toCode {radix : Numerics.Radix} (value : Logarithmic radix) : ofCode value.toCode = value

Rewrapping the code of a logarithmic value returns the original value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Logarithmic.toReal_zero {radix : Numerics.Radix} : zero.toReal = 0

The distinguished logarithmic zero code denotes real zero.

@[simp]

theorem FloatLib.Floats.ExecFloat.Logarithmic.toReal_mul {radix : Numerics.Radix} (left right : Logarithmic radix) : (left.mul right).toReal = left.toReal * right.toReal

Logarithmic multiplication agrees exactly with multiplication of decoded real values.