FP32 rounding tolerances

These theorems express FloatLib's Model.abs_roundAt_sub_le bounds using approxR (notation ≈[t]). Each operation has an absolute-only tolerance of half an ULP at its exact real result. The tolerance therefore depends on the result's magnitude.

FP32 here is a rounded-real model with binary32 precision and an unbounded upper exponent. It has no NaN or infinity values. These are not native Float32 or LibTorch kernel correctness theorems; transcendental operations round the exact real function.

Arithmetic (one real op + one rounding step)

theorem TorchLean.Floats.FP32.add_approxR (a b : FP32) : Proofs.RuntimeApprox.approxR (a.val + b.val) (a + b).val (Proofs.RuntimeApprox.ApproxTol.absOnly (FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (a.val + b.val)))

Rounded addition differs from the exact sum by at most half an ULP.

theorem TorchLean.Floats.FP32.sub_approxR (a b : FP32) : Proofs.RuntimeApprox.approxR (a.val - b.val) (a - b).val (Proofs.RuntimeApprox.ApproxTol.absOnly (FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (a.val - b.val)))

Rounded subtraction differs from the exact difference by at most half an ULP.

theorem TorchLean.Floats.FP32.mul_approxR (a b : FP32) : Proofs.RuntimeApprox.approxR (a.val * b.val) (a * b).val (Proofs.RuntimeApprox.ApproxTol.absOnly (FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (a.val * b.val)))

Rounded multiplication differs from the exact product by at most half an ULP.

theorem TorchLean.Floats.FP32.div_approxR (a b : FP32) : Proofs.RuntimeApprox.approxR (a.val / b.val) (a / b).val (Proofs.RuntimeApprox.ApproxTol.absOnly (FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (a.val / b.val)))

Rounded division follows real division, including its totalized value at zero.

Transcendentals (real function + rounding)

theorem TorchLean.Floats.FP32.exp_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (Real.exp a.val) (FloatLib.Numerics.MathFunctions.exp a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (Real.exp a.val)))

Rounding the exact real exp result introduces at most half an ULP of error.

theorem TorchLean.Floats.FP32.tanh_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (Real.tanh a.val) (FloatLib.Numerics.MathFunctions.tanh a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (Real.tanh a.val)))

Rounding the exact real tanh result introduces at most half an ULP of error.

theorem TorchLean.Floats.FP32.log_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (Real.log a.val) (FloatLib.Numerics.MathFunctions.log a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (Real.log a.val)))

Rounded logarithm uses mathlib's total real logarithm as its reference.

theorem TorchLean.Floats.FP32.cos_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (Real.cos a.val) (FloatLib.Numerics.MathFunctions.cos a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (Real.cos a.val)))

Rounding the exact real cos result introduces at most half an ULP of error.

theorem TorchLean.Floats.FP32.sin_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (Real.sin a.val) (FloatLib.Numerics.MathFunctions.sin a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (Real.sin a.val)))

Rounding the exact real sin result introduces at most half an ULP of error.

theorem TorchLean.Floats.FP32.sinh_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (Real.sinh a.val) (FloatLib.Numerics.MathFunctions.sinh a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (Real.sinh a.val)))

Rounding the exact real sinh result introduces at most half an ULP of error.

theorem TorchLean.Floats.FP32.cosh_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (Real.cosh a.val) (FloatLib.Numerics.MathFunctions.cosh a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (Real.cosh a.val)))

Rounding the exact real cosh result introduces at most half an ULP of error.

theorem TorchLean.Floats.FP32.sqrt_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (√a.val) (FloatLib.Numerics.MathFunctions.sqrt a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 √a.val))

Rounded square root uses mathlib's total real square root as its reference.

theorem TorchLean.Floats.FP32.abs_approxR (a : FP32) : Proofs.RuntimeApprox.approxR |a.val| (FloatLib.Numerics.MathFunctions.abs a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 |a.val|))

Rounding the exact real abs result introduces at most half an ULP of error.

Examples (how this looks in practice)