IEEE32Exec and FP32: Real Semantics Core

Reals view of IEEE32Exec

Real semantics (toReal?/toReal) live in NN.Floats.IEEEExec.Semantics.RealSemantics. This bridge file uses them pervasively, but does not define them.

@[reducible, inline]

noncomputable abbrev TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round (x : ℝ) : ℝ

FP32 rounding viewed as a real function.

Basic checks for fp32Round

theorem TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round_zero : fp32Round 0 = 0

Rounding 0 to float32 yields 0.

Helper lemmas (magnitude/rounding)

Most of the file consists of bridge lemmas: once we decide on the refinement statement, we need many small facts that connect:

• executable bitfield manipulations (extracting sign/exponent/fraction, flipping the sign bit),
• exact dyadic arithmetic (what the decoded value means as a real),
• and the FP32 rounding model (which is expressed using neural_magnitude / nearest-even).

These lemmas are local: they exist to keep the later op-level theorems readable.

noncomputable def TorchLean.Floats.IEEE754.IEEE32Exec.signFactor (s : Bool) : ℝ

theorem TorchLean.Floats.IEEE754.IEEE32Exec.signFactor_xor (a b : Bool) : signFactor (a ^^ b) = signFactor a * signFactor b

theorem TorchLean.Floats.IEEE754.IEEE32Exec.abs_dyadicToReal (d : Dyadic) : |dyadicToReal d| = ↑d.mant * neuralBpow binaryRadix d.exp

Absolute value of a decoded dyadic.

Informal: dyadicToReal d = ± (mant * 2^exp) and since mant ≥ 0, the absolute value is always mant * 2^exp regardless of the sign bit.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal_mul_exact (a b : Dyadic) : dyadicToReal { sign := a.sign ^^ b.sign, mant := a.mant * b.mant, exp := a.exp + b.exp } = dyadicToReal a * dyadicToReal b

Exact multiplication of dyadics commutes with decoding to reals.

Informal: decoding the dyadic that multiplies mantissas and adds exponents gives the product of the decoded real values.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal_neg (d : Dyadic) : dyadicToReal { sign := !d.sign, mant := d.mant, exp := d.exp } = -dyadicToReal d

Negating a dyadic (flipping its sign bit) negates its decoded real value.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.signBit_ofBits_eq_testBit31 (b : UInt32) : (ofBits b).signBit = b.toNat.testBit 31

signBit (ofBits b) is exactly the 31st bit of b at the natural-number level.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.signBit_ofBits_xor_signMask (b : UInt32) : (ofBits (b ^^^ signMask)).signBit = !(ofBits b).signBit

Flipping signMask toggles the sign bit and leaves everything else unchanged.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toDyadic?_neg_of_toDyadic?_some (x : IEEE32Exec) {d : Dyadic} (hx : x.toDyadic? = some d) : x.neg.toDyadic? = some { sign := !d.sign, mant := d.mant, exp := d.exp }

If x decodes to the dyadic d, then neg x decodes to the same magnitude with a flipped sign.

This lemma is one of the bitfield bridge steps that lets us transport algebraic facts from the dyadic semantics to IEEE32Exec.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_neg_eq_neg (x : IEEE32Exec) {d : Dyadic} (hx : x.toDyadic? = some d) : x.neg.toReal = -x.toReal

On finite values, toReal respects IEEE32Exec.neg.

We phrase this as an equality on toReal for convenience, but the proof uses the finiteness witness toDyadic? x = some d.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_posMaxFinite_eq_ieeeMaxFinite : posMaxFinite.toReal = FP32.ieeeMaxFinite

The executable maximum-finite binary32 bit pattern denotes FP32.ieeeMaxFinite.

This identifies the concrete endpoint 0x7f7fffff with the rounded-real guard (2 - 2⁻²³) * 2¹²⁷. Keeping this fact in the core bridge gives overflow and interval proofs a single canonical statement about the upper edge of finite binary32.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.abs_toReal_le_ieeeMaxFinite_of_isFinite (x : IEEE32Exec) (hfin : x.isFinite = true) : |x.toReal| ≤ FP32.ieeeMaxFinite

Every finite executable binary32 value lies between the two maximum-finite endpoints.

The proof reads the stored exponent and fraction fields directly. It covers normal numbers, subnormals, and both signed zeros; NaNs and infinities are excluded by hfin.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_neuralGenericFormat_of_isFinite (x : IEEE32Exec) (hfin : x.isFinite = true) : neuralGenericFormat binaryRadix fexp32 x.toReal

The real denotation of every finite executable binary32 value belongs to the rounded-real binary32 format.

This is the representability bridge from an IEEE bit pattern to fexp32. It is what permits format-level results, such as Sterbenz's lemma, to be applied directly to executable operands.