TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Arithmetic.SignedSemantics.Core

Correctness of binary sign operations #

Negation usually changes only the stored sign bit. Formats with unsigned zero are the exception: their would-be negative-zero word is a reserved NaN, so semantic negation preserves both that NaN and the single zero encoding. This module separates raw sign toggling from policy-aware negation and transports the latter through dyadic decoding to the real semantics.

Reference #

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toggleSign_ofFields (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) :
(ofFields fmt sign exponent fraction).toggleSign = ofFields fmt (!sign) exponent fraction

Toggling an explicitly packed value changes only its supplied sign field.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_ofFields_of_supportsSignedZero (fmt : FloatFormat) (hfmt : fmt.supportsSignedZero = true) (sign : Bool) (exponent fraction : ℕ) :
(ofFields fmt sign exponent fraction).neg = ofFields fmt (!sign) exponent fraction

Packed-field negation toggles the supplied sign when the format represents signed zero.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_copySign {fmt : FloatFormat} (magnitude signSource : Model fmt) :
(magnitude.copySign signSource).fracField = magnitude.fracField

Copying a sign never changes the fraction field.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_copySign {fmt : FloatFormat} (magnitude signSource : Model fmt) :
(magnitude.copySign signSource).expField = magnitude.expField

Copying a sign never changes the exponent field.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_copySign_of_supportsSignedZero {fmt : FloatFormat} (magnitude signSource : Model fmt) (hfmt : fmt.supportsSignedZero = true) :
(magnitude.copySign signSource).signBit = signSource.signBit

In a signed-zero format, copySign gives the magnitude the source's sign.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_copySign {fmt : FloatFormat} (magnitude signSource : Model fmt) :
(magnitude.copySign signSource).isNaN = magnitude.isNaN

Copying a sign preserves NaN classification under every format policy.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_copySign {fmt : FloatFormat} (magnitude signSource : Model fmt) :
(magnitude.copySign signSource).isZero = magnitude.isZero

Copying a sign preserves zero classification under every format policy.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_copySign {fmt : FloatFormat} (magnitude signSource : Model fmt) :
(magnitude.copySign signSource).isInf = magnitude.isInf

Copying a sign preserves infinity classification.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_copySign {fmt : FloatFormat} (magnitude signSource : Model fmt) :
(magnitude.copySign signSource).isFinite = magnitude.isFinite

Copying a sign preserves finiteness.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_abs {fmt : FloatFormat} (x : Model fmt) :
x.abs.isNaN = x.isNaN

Absolute value preserves NaN classification.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_abs {fmt : FloatFormat} (x : Model fmt) :
x.abs.isZero = x.isZero

Absolute value preserves zero classification.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_abs {fmt : FloatFormat} (x : Model fmt) :
x.abs.isInf = x.isInf

Absolute value preserves infinity classification.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_abs {fmt : FloatFormat} (x : Model fmt) :
x.abs.isFinite = x.isFinite

Absolute value preserves finiteness.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_abs_of_supportsSignedZero {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.supportsSignedZero = true) :
x.abs.signBit = false

In a signed-zero format, absolute value clears the stored sign.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_neg {fmt : FloatFormat} (x : Model fmt) :
x.neg.neg = x

Policy-aware negation is involutive for every supported encoding.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_posZero (fmt : FloatFormat) :
(posZero fmt).neg = zero fmt true

Negation maps positive zero to the format's policy-selected negative zero.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_negZero_of_supportsSignedZero (fmt : FloatFormat) (hfmt : fmt.supportsSignedZero = true) :
(negZero fmt).neg = posZero fmt

Negation maps negative zero to positive zero when negative zero is representable.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_posInf (fmt : FloatFormat) :
(posInf fmt).neg = negInf fmt

Negation exchanges the positive and negative IEEE infinity bit patterns in every encoding.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_negInf (fmt : FloatFormat) :
(negInf fmt).neg = posInf fmt

Negation maps the negative IEEE infinity bit pattern to the positive pattern.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_posMinSubnormal (fmt : FloatFormat) :
(posMinSubnormal fmt).signBit = false

The least positive subnormal has sign zero.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_posMinSubnormal (fmt : FloatFormat) :
(posMinSubnormal fmt).isFinite = true

The least positive subnormal is finite in every supported encoding.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_posMinSubnormal (fmt : FloatFormat) :
(posMinSubnormal fmt).isZero = false

The least positive subnormal is nonzero.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_posMinSubnormal (fmt : FloatFormat) :
(posMinSubnormal fmt).isNaN = false

The least positive subnormal is not a NaN.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_posMinSubnormal (fmt : FloatFormat) :
(posMinSubnormal fmt).isInf = false

The least positive subnormal is not an infinity.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.negMinSubnormal_eq_ofFields (fmt : FloatFormat) :
negMinSubnormal fmt = ofFields fmt true 0 1

The negative subnormal of least magnitude is explicit field packing with fraction one.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_negMinSubnormal (fmt : FloatFormat) :
(negMinSubnormal fmt).signBit = true

The negative subnormal of least magnitude has sign one.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_negMinSubnormal (fmt : FloatFormat) :
(negMinSubnormal fmt).isFinite = true

The negative subnormal of least magnitude is finite in every supported encoding.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_negMinSubnormal (fmt : FloatFormat) :
(negMinSubnormal fmt).isZero = false

The negative subnormal of least magnitude is nonzero.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_negMinSubnormal (fmt : FloatFormat) :
(negMinSubnormal fmt).isNaN = false

The negative subnormal of least magnitude is not a NaN.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_negMinSubnormal (fmt : FloatFormat) :
(negMinSubnormal fmt).isInf = false

The negative subnormal of least magnitude is not an infinity.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_posMinSubnormal (fmt : FloatFormat) :
(posMinSubnormal fmt).neg = negMinSubnormal fmt

Negation maps the least positive subnormal to its negative counterpart.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_negMinSubnormal (fmt : FloatFormat) :
(negMinSubnormal fmt).neg = posMinSubnormal fmt

Negation maps the negative subnormal of least magnitude to its positive counterpart.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_maxFinite (fmt : FloatFormat) (sign : Bool) :
(maxFinite fmt sign).signBit = sign

The largest finite encoding carries exactly the requested sign.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_maxFinite (fmt : FloatFormat) (sign : Bool) :
(maxFinite fmt sign).isZero = false

A largest finite encoding is never zero.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_maxFinite (fmt : FloatFormat) (sign : Bool) :
(maxFinite fmt sign).isNaN = false

A largest finite encoding is never a NaN.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_maxFinite (fmt : FloatFormat) (sign : Bool) :
(maxFinite fmt sign).isInf = false

A largest finite encoding is never an infinity.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_maxFinite (fmt : FloatFormat) (sign : Bool) :
(maxFinite fmt sign).neg = maxFinite fmt !sign

Negation toggles the sign of the largest finite magnitude.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_posMaxFinite (fmt : FloatFormat) :
(posMaxFinite fmt).neg = negMaxFinite fmt

Negation maps the largest positive finite value to its negative counterpart.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_negMaxFinite (fmt : FloatFormat) :
(negMaxFinite fmt).neg = posMaxFinite fmt

Negation maps the most negative finite value to its positive counterpart.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_neg {fmt : FloatFormat} (x : Model fmt) :
x.neg.isNaN = x.isNaN

Negation preserves NaN classification, including the reserved NaN of unsigned-zero formats.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_neg {fmt : FloatFormat} (x : Model fmt) :
x.neg.isInf = x.isInf

Negation preserves infinity classification.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_neg {fmt : FloatFormat} (x : Model fmt) :
x.neg.isZero = x.isZero

Negation preserves zero classification.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_neg {fmt : FloatFormat} (x : Model fmt) :
x.neg.isFinite = x.isFinite

Negation preserves finiteness.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Numerics.Dyadic.toReal_mk_not_negative (d : Numerics.Dyadic) :
{ negative := !d.negative, significand := d.significand, exponent := d.exponent }.toReal = -d.toReal

Flipping the sign flag of a dyadic negates its real value, including for zero significands.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic?_neg_of_toDyadic?_some {fmt : FloatFormat} (x : Model fmt) {d : Numerics.Dyadic} (hx : x.toDyadic? = some d) :
x.neg.toDyadic? = some (negDyadic fmt d)

Policy-aware negation decodes to exact dyadic negation with the format's zero convention.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Numerics.Dyadic.toReal_negDyadic (fmt : FloatFormat) (d : Numerics.Dyadic) :
(negDyadic fmt d).toReal = -d.toReal

Format-aware dyadic negation is real-number negation.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_neg {fmt : FloatFormat} (x : Model fmt) (hx : x.isFinite = true) :
x.neg.toReal = -x.toReal

On finite values, executable policy negation is real-number negation.