Exact absolute values and encoded sign operations

The sign and quiet-NaN bits occupy distinct positions for every binary descriptor. Consequently encoded absolute value preserves signaling status and payload. In a signed-zero format it also clears the sign of every value, giving the exact-value bridge used by magnitude ordering. Unsigned-zero formats preserve their reserved NaN word under encoded absolute value. The bridge therefore requires a format that supports signed zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic?_abs_of_supportsSignedZero {fmt : FloatFormat} {x : Model fmt} (hfmt : fmt.supportsSignedZero = true) {d : Numerics.Dyadic} (hx : x.toDyadic? = some d) : x.abs.toDyadic? = some { negative := false, significand := d.significand, exponent := d.exponent }

In a signed-zero format, encoded absolute value clears exactly the decoded dyadic sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exactValue_abs_of_supportsSignedZero {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.supportsSignedZero = true) : x.abs.exactValue = x.exactValue.abs

Exact interpretation commutes with absolute value whenever every sign can be cleared.