TorchLean API

Docs HomeGuideExamplesGraphs

NN.Floats.IEEEExec.TrigRules

Deterministic trigonometric special-value rules (sin, cos) #

NN.Floats.IEEEExec.Exec32 defines deterministic, executable IEEE32Exec.sin and IEEE32Exec.cos (implemented purely inside Lean; no delegation to the host Float runtime).

This file exposes the special-case rewrite rules (NaN/Inf/±0) so downstream proofs do not need to unfold the whole implementation.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.sin_eq_quietNaN_of_isNaN (x : IEEE32Exec) (hx : x.isNaN = true) :
x.sin = x.quietNaN

sin propagates NaNs by returning the quieted payload.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.cos_eq_quietNaN_of_isNaN (x : IEEE32Exec) (hx : x.isNaN = true) :
x.cos = x.quietNaN

cos propagates NaNs by returning the quieted payload.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.sin_posInf :
posInf.sin = canonicalNaN

sin(±Inf) = NaN.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.sin_negInf :
negInf.sin = canonicalNaN

sin(±Inf) = NaN.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.cos_posInf :
posInf.cos = canonicalNaN

cos(±Inf) = NaN.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.cos_negInf :
negInf.cos = canonicalNaN

cos(±Inf) = NaN.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.sin_posZero :
posZero.sin = posZero

sin(+0) = +0.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.sin_negZero :
negZero.sin = negZero

sin(-0) = -0.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.cos_posZero :
posZero.cos = ofBits 1065353216

cos(±0) = 1.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.cos_negZero :
negZero.cos = ofBits 1065353216

cos(±0) = 1.