Executable binary32 transcendental approximations.

The functions in this file provide deterministic exp, log, and related operations for the IEEE32 executable model. Stronger libm-style correctness claims live outside this layer.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedScale : ℕ

Fixed-point scale (in bits) used by the integer-only exp/log approximations.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedScaleInt : ℤ

fixedScale as an Int.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedOne : ℤ

Fixed-point encoding of 1 at scale fixedScale (i.e. 2^fixedScale).

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.pow2Int (k : ℕ) : ℤ

Integer power of two: pow2Int k = 2^k as an Int.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.roundQuotEvenInt (num den : ℤ) : ℤ

Round an integer quotient num/den to the nearest integer, ties-to-even.

Assumes den > 0.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.roundDivPow2EvenInt (n : ℤ) (shift : ℕ) : ℤ

Divide by 2^shift, rounding to nearest with ties-to-even.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.shiftPow2EvenInt (n k : ℤ) : ℤ

Shift by a power of two: multiply when k ≥ 0, divide when k < 0.

Division uses ties-to-even rounding.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedMul (a b : ℤ) : ℤ

Fixed-point multiplication at scale fixedScale (ties-to-even).

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedDiv (a b : ℤ) : ℤ

Fixed-point division at scale fixedScale (ties-to-even).

If a and b are fixed-point at scale fixedScale, the result is at the same scale.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedDivByNat (a : ℤ) (n : ℕ) : ℤ

Divide by a natural number, rounding to nearest with ties-to-even.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedOfDyadic (d : Dyadic) : ℤ

Convert a dyadic number to a signed fixed-point integer at scale fixedScale.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedToDyadic (x : ℤ) : Dyadic

Convert a signed fixed-point integer at scale fixedScale to a dyadic number.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedLn2 : ℤ

Fixed-point approximation to ln 2 at scale fixedScale.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.fixedInvLn2 : ℤ

Fixed-point approximation to 1/ln 2 at scale fixedScale.

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.exp2PolyCoeffsDesc : List ℤ

Fixed-point Taylor coefficients (highest degree first) for 2^x on [-1/2, 1/2].

def TorchLean.Floats.IEEE754.IEEE32Exec.Transcendentals.evalExp2Poly (xFixed : ℤ) : ℤ

Evaluate the fixed-point 2^x polynomial approximation using Horner’s method.

def TorchLean.Floats.IEEE754.IEEE32Exec.exp (x : IEEE32Exec) : IEEE32Exec

Deterministic exp (no delegation to Float): range-reduced 2^(x/ln2) with a fixedpoint polynomial.

def TorchLean.Floats.IEEE754.IEEE32Exec.log (x : IEEE32Exec) : IEEE32Exec

Deterministic log (no delegation to Float): normalize x = m*2^k and use an atanh-series for log m.

def TorchLean.Floats.IEEE754.IEEE32Exec.sinh (x : IEEE32Exec) : IEEE32Exec

Deterministic sinh (no delegation to Float): defined via exp.

def TorchLean.Floats.IEEE754.IEEE32Exec.cosh (x : IEEE32Exec) : IEEE32Exec

Deterministic cosh (no delegation to Float): defined via exp.

def TorchLean.Floats.IEEE754.IEEE32Exec.tanh (x : IEEE32Exec) : IEEE32Exec

Deterministic tanh (no delegation to Float): stable form tanh x = s*(1 - 2/(exp(2*|x|)+1)).

Deterministic sin/cos

Unlike exp/log, sin and cos are used by the runtime FFT layer (NN.Runtime.*.Fft) to build twiddle factors. Delegating to the host Float implementation makes results platform-dependent.

We implement sin/cos purely inside Lean:

1. scale the input down by a power of two so |y| < 1/2,
2. approximate sin y and cos y by exact Taylor partial sums (degree 13 / 12),
3. scale back up using m applications of the double-angle formulas.

This is deterministic and uses only the IEEE32Exec kernel ops (roundRatToIEEE32, add/mul/sub, etc.). We do not claim correctly-rounded libm behavior; the goal is reproducible execution.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.mulDyadic (a b : Dyadic) : Dyadic

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.oneDyadic : Dyadic

Dyadic 1.

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.roundDyadicDivNat (d : Dyadic) (den : ℕ) : IEEE32Exec

Round the exact rational d / den to binary32, where d is an exact dyadic mant * 2^exp.

We package the dyadic exponent into a rational numerator/denominator and call roundRatToIEEE32.

Taylor partial sums on |y| < 1/2

We encode the partial sums using a common factorial denominator so the coefficients are exact integers, not approximations.

For z = y^2:

• sin y = ∑_{i=0}^6 (-1)^i y^(2i+1)/(2i+1)! + R₇(y) where the polynomial part can be written as y * (∑_{i=0}^6 (-1)^i (13!/(2i+1)!) z^i) / 13!.

• cos y = ∑_{i=0}^6 (-1)^i y^(2i)/(2i)! + R₇'(y) i.e. (∑_{i=0}^6 (-1)^i (12!/(2i)!) z^i) / 12!.

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.sinDen : ℕ

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.cosDen : ℕ

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.sinCoeff (i : ℕ) : ℤ

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.cosCoeff (i : ℕ) : ℤ

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.coeffToDyadic (c : ℤ) : Dyadic

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.evalPolyNumerator (coeff : ℕ → ℤ) (z : Dyadic) : Dyadic

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.sinCosTaylorSmall (y : Dyadic) : IEEE32Exec × IEEE32Exec

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.doubleAngle (sc : IEEE32Exec × IEEE32Exec) : IEEE32Exec × IEEE32Exec

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.iterDoubleAngle : ℕ → IEEE32Exec × IEEE32Exec → IEEE32Exec × IEEE32Exec

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.sinCosPow2 (y : Dyadic) (m : ℕ) : IEEE32Exec × IEEE32Exec

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.sinCosScaled (dx : Dyadic) : IEEE32Exec × IEEE32Exec

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.sinCos (x : IEEE32Exec) : IEEE32Exec × IEEE32Exec

Joint deterministic sin/cos computation for IEEE32Exec.

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.sin (x : IEEE32Exec) : IEEE32Exec

Deterministic sin implementation (shared core via sinCos).

def TorchLean.Floats.IEEE754.IEEE32Exec.Trig.cos (x : IEEE32Exec) : IEEE32Exec

Deterministic cos implementation (shared core via sinCos).

Public sin / cos

We expose sin/cos as executable ops on IEEE32Exec using the deterministic implementation above, together with standard IEEE special-case conventions.

def TorchLean.Floats.IEEE754.IEEE32Exec.sin (x : IEEE32Exec) : IEEE32Exec

Deterministic sin for IEEE32Exec.

def TorchLean.Floats.IEEE754.IEEE32Exec.cos (x : IEEE32Exec) : IEEE32Exec

Deterministic cos for IEEE32Exec.