BridgeFP32

Bridge theorems: IEEE32Exec (a bit-level, executable IEEE-754 binary32 kernel) ↔ FP32 (a Flocq-style “round-to-ℝ” model for finite float32 computations).

TorchLean keeps two views of float32:

• Executable view (IEEE32Exec): we can run models inside Lean by implementing IEEE-754-style operations on the raw 32-bit encoding.
• Mathematical view (FP32): we can reuse a large amount of existing floating-point theory (rounding, ulps, error bounds) phrased as real arithmetic + a rounding operator.

This file bridges those two views. Informally, the main statements have the shape:

toReal (op_exec x y) = fp32Round (op_real (toReal x) (toReal y))

under the side-condition that we stay on the finite / no-overflow path. That is exactly the “refinement” we need to justify using FP32/NF reasoning when our runtime execution is driven by IEEE32Exec.

What we do not claim here:

• FP32 models only finite values, so NaNs/Infs are not bridged (proofs use toReal? and carry “isFinite = true” hypotheses).
• Some transcendental functions in IEEE32Exec exist for executability but are not part of the verified IEEE kernel; this file therefore focuses on the core arithmetic and the reductions we rely on in practice.

Pointers / background:

• IEEE 754-2019 (rounding modes, signed zeros, specials): https://doi.org/10.1109/IEEESTD.2019.8766229
• Goldberg (1991), a classic practical guide to IEEE-754 reasoning: https://doi.org/10.1145/103162.103163
• Higham (2002), error analysis in finite precision (book): ISBN 0-89871-521-0
• Flocq (Boldo–Melquiond, 2011), a widely-used formal floating-point library design: https://doi.org/10.1109/ARITH.2011.40
• Boldo et al. (2012), “Floating-point arithmetic in the Coq system”: https://doi.org/10.1016/j.ic.2011.09.005

Reals view of IEEE32Exec

Real semantics (toReal?/toReal) live in NN.Floats.IEEEExec.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 sanity 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.

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.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 fundamentally uses the finiteness witness toDyadic? x = some d.

Exact dyadic addition (used by op-level refinement theorems)

IEEE-754 addition is “exact add, then round”. To connect an executable add to the FP32 model, we factor the refinement into two steps:

1. perform an exact addition in an unbounded format (here: dyadics with integer exponents), and
2. apply float32 rounding.

addDyadic is our exact step (it aligns exponents, adds signed mantissas, and normalizes), and the lemmas in this section show that its real interpretation is literally real addition.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal_addDyadic_exact (a b : Dyadic) : dyadicToReal (addDyadic a b) = dyadicToReal a + dyadicToReal b

addDyadic is exact with respect to dyadicToReal.

Informal: addDyadic aligns exponents, adds signed mantissas, and normalizes; decoding the result gives the sum of the decoded inputs.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.neural_magnitude_dyadic (d : Dyadic) (hm : d.mant ≠ 0) : neuralMagnitude binaryRadix (dyadicToReal d) = Int.ofNat (Nat.log 2 d.mant) + d.exp + 1

For a nonzero dyadic, neural_magnitude matches the expected “power-of-two interval” characterization: mag = ⌊logb 2 (mant)⌋ + exp + 1.

We use this as a key link between the FP32 rounding model (defined using neural_magnitude) and the executable kernel (which naturally computes Nat.log2 mant + exp from the decoded dyadic).

Signed nearest-even (and power-of-two specialization)

FP32 uses “round to nearest, ties to even” (IEEE 754's default). The executable kernel implements the same policy, but at the level of integer arithmetic on mantissas.

In this section we establish basic algebraic properties of nearest-even rounding that we can reuse later when relating the IEEE32Exec rounding code to fp32Round.

Real semantics of exponent tests for rationals

Some executable rounding code works by inspecting the magnitude of a rational (represented as num / den with Nats) and branching on exponent ranges. These lemmas justify those branches in terms of real inequalities, so later refinement proofs can stay “math-first”.

Coarse log₂ bounds for rationals

The rounding code needs cheap bounds on log₂ (or “bit-length”) to decide normal vs subnormal cases. We prove coarse but robust bounds that are easy to compute from Nat.log2.

FP32 refinement for executable rounding

This is the core bridge step: we prove that the executable rounding kernel (which produces an IEEE32Exec value) agrees with FP32 rounding on reals (fp32Round), provided we stay on the finite/no-overflow path.

Once we have this, most op-level bridge theorems reduce to: “compute an exact dyadic/rational intermediate, then apply this rounding refinement theorem”.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.abs_dyadicToReal_lt_bpow_succ_log2 (d : Dyadic) : |dyadicToReal d| < neuralBpow binaryRadix (Int.ofNat d.mant.log2 + d.exp + 1)

A coarse magnitude bound for a decoded dyadic.

Informal: |mant * 2^exp| < 2^(log2 mant + exp + 1). This is convenient when reasoning about normalization by log2 and when relating dyadic magnitudes to exponent ranges.

Signed zeros

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_signedZero (s : Bool) : (if s = true then negZero else posZero).toReal = 0

Both +0 and -0 decode to the real number 0.

IEEE-754 has signed zeros because they matter for some operations (notably division and some transcendentals). Our finite FP32 model treats them as equal at the real level, and the bridge lemmas in this file use this fact repeatedly.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_posZero : posZero.toReal = 0

+0 decodes to the real number 0.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_negZero : negZero.toReal = 0

-0 decodes to the real number 0.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_roundDyadicToIEEE32_eq_fp32Round (d : Dyadic) (hfin : (roundDyadicToIEEE32 d).isFinite = true) : (roundDyadicToIEEE32 d).toReal = fp32Round (dyadicToReal d)

Refinement theorem (finite/no-overflow): rounding an exact dyadic with the executable IEEE32 kernel agrees with the Flocq-style FP32 rounding-on-ℝ model.

The hypothesis isFinite (roundDyadicToIEEE32 d) = true rules out the overflow-to-±Inf branches.

Rounding rationals (finite/no-overflow)

Some operations (notably division and parts of transcendental approximations) naturally produce rationals num / den. The executable kernel rounds those rationals to float32 by:

• classifying magnitude (normal/subnormal/underflow/overflow),
• computing a scaled mantissa,
• applying nearest-even,
• and assembling the output bits.

This section connects that algorithm to the FP32 real rounding model.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_roundRatToIEEE32_eq_fp32Round (sign : Bool) (num den : ℕ) (hden : den ≠ 0) (hfin : (roundRatToIEEE32 sign num den).isFinite = true) : (roundRatToIEEE32 sign num den).toReal = fp32Round ((if sign = true then -1 else 1) * (↑num / ↑den))

Refinement theorem (finite/no-overflow): rounding an exact rational with the executable IEEE32 kernel agrees with the Flocq-style FP32 rounding-on-ℝ model.

The hypothesis isFinite (roundRatToIEEE32 sign num den) = true rules out the overflow-to-±Inf branches.

Op-level refinement theorems (finite/no-overflow)

These are the results that the rest of TorchLean typically consumes: statements that each arithmetic operation in IEEE32Exec refines its FP32 real-rounded counterpart.

If you are coming from PyTorch: this is the “float32 math model” that underlies many informal numerical arguments (“the kernel computes the exact real result, then rounds to float32”), but made explicit and proved for our executable kernel.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_add_eq_fp32Round (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hfin : (x.add y).isFinite = true) : (x.add y).toReal = fp32Round (x.toReal + y.toReal)

Finite refinement for addition: IEEE32Exec.add = exact real add + float32 rounding.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sub_eq_fp32Round (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hfin : (x.sub y).isFinite = true) : (x.sub y).toReal = fp32Round (x.toReal - y.toReal)

Finite refinement for subtraction, reduced to addition + negation.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_mul_eq_fp32Round (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hfin : (x.mul y).isFinite = true) : (x.mul y).toReal = fp32Round (x.toReal * y.toReal)

Finite refinement for multiplication: IEEE32Exec.mul = exact real mul + float32 rounding.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_fma_eq_fp32Round (x y z : IEEE32Exec) {dx dy dz : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hz : z.toDyadic? = some dz) (hfin : (x.fma y z).isFinite = true) : (x.fma y z).toReal = fp32Round (x.toReal * y.toReal + z.toReal)

Finite refinement for fused multiply-add: fma x y z rounds x*y + z once at the end.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_div_eq_fp32Round (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hy0 : dy.mant ≠ 0) (hfin : (x.div y).isFinite = true) : (x.div y).toReal = fp32Round (x.toReal / y.toReal)

Finite refinement for division.

At the executable level, division is implemented by forming an exact rational quotient num/den (after aligning dyadic exponents) and then rounding that rational to float32. This theorem states that the overall real meaning is FP32 rounding of real division.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sqrt_eq_fp32Round (x : IEEE32Exec) {dx : Dyadic} (hx : x.toDyadic? = some dx) (hfin : x.sqrt.isFinite = true) : x.sqrt.toReal = fp32Round √x.toReal

Finite refinement for square root.

IEEE32Exec.sqrt computes an executable approximation and then rounds it to float32. This bridge theorem states that, on the finite path, the real meaning agrees with FP32 rounding of Real.sqrt.

Comparisons and min/max (finite refinement)

Comparisons are subtle in IEEE-754 because of NaNs and signed zeros. Since FP32 is a finite-only model, we only bridge the finite behavior here: comparisons/min/max agree with the corresponding real comparisons once NaNs/Infs are ruled out.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.cmpDyadic_lt_iff (a b : Dyadic) : cmpDyadic a b = Ordering.lt ↔ dyadicToReal a < dyadicToReal b

Dyadic comparison correctness (lt case).

cmpDyadic compares two decoded dyadics by aligning exponents and comparing signed integers. This theorem states that the .lt result agrees with the real-ordering of dyadicToReal.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.cmpDyadic_eq_iff (a b : Dyadic) : cmpDyadic a b = Ordering.eq ↔ dyadicToReal a = dyadicToReal b

Dyadic comparison correctness (eq case).

This is the equality variant of cmpDyadic_lt_iff.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.cmpDyadic_gt_iff (a b : Dyadic) : cmpDyadic a b = Ordering.gt ↔ dyadicToReal b < dyadicToReal a

Dyadic comparison correctness (gt case).

This is the greater-than variant of cmpDyadic_lt_iff, phrased as dyadicToReal b < dyadicToReal a.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.compare_eq_some_cmpDyadic_of_toDyadic? (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.compare y = some (cmpDyadic dx dy)

Bridge for IEEE32Exec.compare on finite values.

When both operands decode to dyadics (toDyadic? = some), compare returns a result and it is exactly cmpDyadic of those dyadics.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.compare_eq_some_lt_iff_toReal_lt (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.compare y = some Ordering.lt ↔ x.toReal < y.toReal

compare x y = .lt if and only if toReal x < toReal y (finite path).

This is the user-facing ordering theorem that lets downstream reasoning switch between IEEE32Exec.compare and < on reals.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.compare_eq_some_eq_iff_toReal_eq (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.compare y = some Ordering.eq ↔ x.toReal = y.toReal

compare x y = .eq if and only if toReal x = toReal y (finite path).

Note: this equality is on the decoded real values; it ignores NaN payloads and signed-zero distinctions (those are handled explicitly elsewhere).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.compare_eq_some_gt_iff_toReal_gt (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.compare y = some Ordering.gt ↔ y.toReal < x.toReal

compare x y = .gt if and only if toReal y < toReal x (finite path).

This is the greater-than companion to compare_eq_some_lt_iff_toReal_lt.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_minimum_eq_min (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : (x.minimum y).toReal = min x.toReal y.toReal

Bridge for IEEE32Exec.minimum on finite values: its real meaning is min (toReal x) (toReal y).

This proof follows IEEE-754 style rules (including NaN propagation and signed-zero handling), but the statement is on toReal, which erases the sign of zero.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_maximum_eq_max (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : (x.maximum y).toReal = max x.toReal y.toReal

Bridge for IEEE32Exec.maximum on finite values: its real meaning is max (toReal x) (toReal y).

This is the companion of toReal_minimum_eq_min. As above, the conclusion is phrased in terms of toReal, so signed zeros are identified.