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/\log 2}$,
• log: normalization $x=m2^k$ + a convergent atanh-series for $\log m$,
• sinh, cosh: defined via exp,
• tanh: a small-input odd polynomial plus a bounded 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 Lean definitions prioritize reproducibility and well-defined behavior.

Finite approximation contracts

The deterministic functions in this module have proved special-value behavior below. A numerical accuracy claim on finite inputs requires a separate contract. Keeping that evidence explicit prevents reproducible execution from being mistaken for correct rounding.

structure TorchLean.Floats.IEEE754.IEEE32Exec.UnaryApproximationContract (impl : IEEE32Exec → IEEE32Exec) (spec : ℝ → ℝ) (domain : ℝ → Prop) (tolerance : ℝ) : Prop

A uniform real-error contract for an executable unary binary32 operation on a stated domain.

For every finite input whose real value lies in domain, the executable result must also be finite and differ from spec by at most tolerance.

• tolerance_nonneg : 0 ≤ tolerance
• error_le (x : IEEE32Exec) (xr : ℝ) : x.toReal? = some xr → domain xr → ∃ (yr : ℝ), (impl x).toReal? = some yr ∧ |yr - spec xr| ≤ tolerance

theorem TorchLean.Floats.IEEE754.IEEE32Exec.UnaryApproximationContract.mono {impl : IEEE32Exec → IEEE32Exec} {spec : ℝ → ℝ} {domain : ℝ → Prop} {tolerance tolerance' : ℝ} (h : UnaryApproximationContract impl spec domain tolerance) (hle : tolerance ≤ tolerance') : UnaryApproximationContract impl spec domain tolerance'

A proved approximation contract remains valid when its tolerance is weakened.

exp

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

• $\exp(\mathrm{NaN})=\mathrm{NaN}$ (we quiet signaling NaNs),
• $\exp(+\infty)=+\infty$,
• $\exp(-\infty)=+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(+\infty)=+\infty$.

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

$\exp(-\infty)=+0$.

log

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

• $\log(\mathrm{NaN})=\mathrm{NaN}$ (quieted),
• $\log(+\infty)=+\infty$,
• $\log(0)=-\infty$ (for both $+0$ and $-0$),
• $\log(x)=\mathrm{NaN}$ for $x<0$ (including $\log(-\infty)$).

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(+\infty)=+\infty$.

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

$\log(-\infty)=\mathrm{NaN}$ (domain error for negative inputs).

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

$\log(+0)=-\infty$.

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

$\log(-0)=-\infty$.

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,+\infty)\to\mathbb{R}$, transported to the float32 setting (excluding NaNs, infinities, and zeros, which are handled by earlier branches).

tanh

Special values we follow:

• $\tanh(\mathrm{NaN})=\mathrm{NaN}$ (quieted),
• $\tanh(+\infty)=+1$,
• $\tanh(-\infty)=-1$.

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

• 0x3F800000 represents $+1$,
• 0xBF800000 represents $-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(+\infty)=+1$.

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

$\tanh(-\infty)=-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(\pm\infty)=\pm\infty$,
• $\cosh(\pm\infty)=+\infty$.

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(+\infty)=+\infty$.

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

$\sinh(-\infty)=-\infty$.

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

$\cosh(+\infty)=+\infty$.

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

$\cosh(-\infty)=+\infty$.