Signed extended-real interpretation of binary models

Executable, policy-aware negation reverses the extended-real interpretation of every non-NaN value. The result applies uniformly to finite values and infinities; only NaNs are excluded.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_ite {fmt : FloatFormat} {p : Prop} [Decidable p] (x y : Model fmt) : (if p then x else y).neg = if p then x.neg else y.neg

Executable float negation distributes over a conditional choice.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_neg_of_isNaN_eq_false {fmt : FloatFormat} (x : Model fmt) (hnan : x.isNaN = false) : x.neg.toEReal = -x.toEReal

Negating any non-NaN executable float negates its extended-real interpretation.