Lemmas about sign-bit flips (b ^^^ signMask)

The executable IEEE32 kernel implements negation by flipping the sign bit of the underlying UInt32 encoding. For many proofs (finite/special classification, interval soundness, bridge lemmas) we need the basic fact that this operation does not affect the exponent or fraction fields.

This file centralizes those bit-manipulation lemmas for the large proof modules.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.expField_ofBits_xor_signMask (b : UInt32) : (ofBits (b ^^^ signMask)).expField = (ofBits b).expField

Flipping the sign bit of a float32 encoding does not affect its exponent field.

We use this to show that IEEE32Exec.neg preserves the “finite vs NaN/Inf” classification, because NaN/Inf are detected from exponent+fraction (not from sign).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.fracField_ofBits_xor_signMask (b : UInt32) : (ofBits (b ^^^ signMask)).fracField = (ofBits b).fracField

Flipping the sign bit of a float32 encoding does not affect its fraction field.

This complements expField_ofBits_xor_signMask: NaN payload bits are unchanged.