Deterministic transcendental functions (exp, log, tanh, sinh, cosh)

IEEE-754 fixes the representation and the basic arithmetic operations, but it does not mandate exact bit-level behavior for transcendental functions like exp and log. In practice, libraries (libm, SVML, CUDA math, etc.) make slightly different choices, and results can differ across platforms.

In TorchLean, we still need executable transcendental operations in some examples and runtime experiments. So we give IEEE32Exec deterministic definitions for a small set of functions using fixed algorithms:

• exp: range reduction + a fixed-point polynomial for 2^(x/ln 2),
• log: normalization x = m * 2^k + a convergent atanh-series for log m,
• sinh, cosh: defined via exp,
• tanh: a numerically stable expression in terms of exp.

Here we prove the special-value rules for those definitions: how NaNs, infinities, signed zeros (+0 and -0), and sign checks behave. These are the facts we want in proofs without unfolding the full fixed-point implementations.

We do not claim that the finite-value approximations match any particular hardware expf/logf; the goal is reproducibility (and well-defined behavior) inside Lean.

exp

Special values we follow (common libm / PyTorch behavior):

• exp(NaN) = NaN (we quiet signaling NaNs),
• exp(+Inf) = +Inf,
• exp(-Inf) = +0.

For finite inputs, Exec32.lean defines a deterministic approximation. These lemmas only expose the early "special-case" branches, so proofs do not have to unfold the fixed-point core.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.exp_eq_quietNaN_of_isNaN (x : IEEE32Exec) (hx : x.isNaN = true) : x.exp = x.quietNaN

exp propagates NaNs by returning the quieted NaN payload.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.exp_posInf : posInf.exp = posInf

exp(+Inf) = +Inf.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.exp_negInf : negInf.exp = posZero

exp(-Inf) = +0.

log

The special cases match the usual real-analytic extension used by common libraries:

• log(NaN) = NaN (quieted),
• log(+Inf) = +Inf,
• log(0) = -Inf (for both +0 and -0),
• log(x < 0) = NaN (including log(-Inf)).

PyTorch follows these conventions on IEEE hardware; we mirror them in IEEE32Exec.log.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.log_eq_quietNaN_of_isNaN (x : IEEE32Exec) (hx : x.isNaN = true) : x.log = x.quietNaN

log propagates NaNs by returning the quieted NaN payload.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.log_posInf : posInf.log = posInf

log(+Inf) = +Inf.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.log_negInf : negInf.log = canonicalNaN

log(-Inf) = NaN (domain error for negative inputs).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.log_posZero : posZero.log = negInf

log(+0) = -Inf.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.log_negZero : negZero.log = negInf

log(-0) = -Inf.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.log_eq_canonicalNaN_of_negative (x : IEEE32Exec) (hxNaN : x.isNaN = false) (hxInf : x.isInf = false) (hxZero : x.isZero = false) (hxSign : x.signBit = true) : x.log = canonicalNaN

log returns canonicalNaN on negative finite inputs (domain error).

This captures the standard real domain restriction log : (0, +∞) → ℝ, transported to the float32 setting (excluding NaNs/Infs/zeros which are handled by earlier branches).

tanh

Special values we follow:

• tanh(NaN) = NaN (quieted),
• tanh(+Inf) = +1,
• tanh(-Inf) = -1.

The bit patterns used below are the IEEE-754 binary32 encodings of +1.0f and -1.0f:

• 0x3F800000 = +1,
• 0xBF800000 = -1.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.tanh_eq_quietNaN_of_isNaN (x : IEEE32Exec) (hx : x.isNaN = true) : x.tanh = x.quietNaN

tanh propagates NaNs by returning the quieted NaN payload (via chooseNaN1).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.tanh_posInf : posInf.tanh = ofBits 1065353216

tanh(+Inf) = +1.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.tanh_negInf : negInf.tanh = ofBits 3212836864

tanh(-Inf) = -1.

sinh / cosh

These are defined in Exec32.lean in terms of exp (with a NaN short-circuit up front), so the special cases are the familiar ones:

• propagate NaNs (quieted),
• sinh(±Inf) = ±Inf,
• cosh(±Inf) = +Inf.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.sinh_eq_quietNaN_of_isNaN (x : IEEE32Exec) (hx : x.isNaN = true) : x.sinh = x.quietNaN

sinh propagates NaNs by returning the quieted NaN payload (via chooseNaN1).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.cosh_eq_quietNaN_of_isNaN (x : IEEE32Exec) (hx : x.isNaN = true) : x.cosh = x.quietNaN

cosh propagates NaNs by returning the quieted NaN payload (via chooseNaN1).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.sinh_posInf : posInf.sinh = posInf

sinh(+Inf) = +Inf.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.sinh_negInf : negInf.sinh = negInf

sinh(-Inf) = -Inf.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.cosh_posInf : posInf.cosh = posInf

cosh(+Inf) = +Inf.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.cosh_negInf : negInf.cosh = posInf

cosh(-Inf) = +Inf.