Bridging FP32 error bounds into ≈[t]

NN.Proofs.RuntimeApprox.Core.Tolerance defines a small “close enough” relation:

• approxR x y t (notation: x ≈[t] y)

Here we connect that generic notion of tolerance to our FP32 rounding model.

In NN.Floats.FP32.Error we prove per‑operation absolute error bounds like

abs (approx - exact) ≤ eps₃₂ exact

We repackage those bounds so downstream proofs can use the uniform ≈[t] vocabulary.

Two small conventions show up everywhere below:

• We use an absolute-only tolerance ApproxTol.absOnly eps. That means x ≈[absOnly eps] y is literally the usual bound |y - x| ≤ eps (see approxR_absOnly_iff). This matches the shape of our FP32 theorems.

• The FP32 “epsilon” is value-dependent: eps = ulp(exact) / 2 = eps₃₂(exact). This is the standard round-to-nearest error model: the ulp is smaller near 0 and grows as the magnitude grows. Writing it as an ≈[t] fact makes it easy to mix with other tolerances without inventing yet another approximation relation.

The next two lemmas are local rewrite helpers:

• approxR_absOnly_of_abs_sub_le turns a plain abs (y - x) ≤ eps inequality into an approxR.
• eps32_nonneg is the nonnegativity proof we need to use approxR_absOnly_iff.

They are private because they are only used by this file's approximation bridge.

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 (eps₃₂ (a.val + b.val)))

FP32 addition, stated as an ≈[t] fact with t = absOnly (ulp(exact)/2).

Read this as:

• “the exact real sum” is a.val + b.val,
• “the rounded result” is (a + b).val,
• and the two differ by at most half an ulp of the exact real sum.

Informal: a.val + b.val ≈[absOnly (eps₃₂(a.val + b.val))] (a + b).val.

theorem TorchLean.Floats.FP32.sub_approxR (a b : FP32) : Proofs.RuntimeApprox.approxR (a.val - b.val) (a - b).val (Proofs.RuntimeApprox.ApproxTol.absOnly (eps₃₂ (a.val - b.val)))

FP32 subtraction, stated as an ≈[t] fact with t = absOnly (eps₃₂(exact)).

Informal: a.val - b.val ≈[absOnly (eps₃₂(a.val - b.val))] (a - b).val.

theorem TorchLean.Floats.FP32.mul_approxR (a b : FP32) : Proofs.RuntimeApprox.approxR (a.val * b.val) (a * b).val (Proofs.RuntimeApprox.ApproxTol.absOnly (eps₃₂ (a.val * b.val)))

FP32 multiplication, stated as an ≈[t] fact with t = absOnly (eps₃₂(exact)).

Informal: a.val * b.val ≈[absOnly (eps₃₂(a.val * b.val))] (a * b).val.

theorem TorchLean.Floats.FP32.div_approxR (a b : FP32) : Proofs.RuntimeApprox.approxR (a.val / b.val) (a / b).val (Proofs.RuntimeApprox.ApproxTol.absOnly (eps₃₂ (a.val / b.val)))

FP32 division, stated as an ≈[t] fact with t = absOnly (eps₃₂(exact)).

Informal: a.val / b.val ≈[absOnly (eps₃₂(a.val / b.val))] (a / b).val.

Transcendentals (real function + rounding)

theorem TorchLean.Floats.FP32.exp_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (Real.exp a.val) (MathFunctions.exp a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (eps₃₂ (Real.exp a.val)))

FP32 exp is Real.exp followed by rounding; this is the result as an ≈[t] statement.

Informal: exp(a.val) ≈[absOnly (eps₃₂(exp(a.val)))] (exp a).val.

theorem TorchLean.Floats.FP32.tanh_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (Real.tanh a.val) (MathFunctions.tanh a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (eps₃₂ (Real.tanh a.val)))

FP32 tanh as an ≈[t] statement.

Informal: tanh(a.val) ≈[absOnly (eps₃₂(tanh(a.val)))] (tanh a).val.

theorem TorchLean.Floats.FP32.log_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (Real.log a.val) (MathFunctions.log a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (eps₃₂ (Real.log a.val)))

FP32 log as an ≈[t] statement (using Real.log as the exact reference).

Informal: log(a.val) ≈[absOnly (eps₃₂(log(a.val)))] (log a).val.

theorem TorchLean.Floats.FP32.cos_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (Real.cos a.val) (MathFunctions.cos a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (eps₃₂ (Real.cos a.val)))

FP32 cos as an ≈[t] statement.

Informal: cos(a.val) ≈[absOnly (eps₃₂(cos(a.val)))] (cos a).val.

theorem TorchLean.Floats.FP32.sin_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (Real.sin a.val) (MathFunctions.sin a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (eps₃₂ (Real.sin a.val)))

FP32 sin as an ≈[t] statement.

Informal: sin(a.val) ≈[absOnly (eps₃₂(sin(a.val)))] (sin a).val.

theorem TorchLean.Floats.FP32.sinh_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (Real.sinh a.val) (MathFunctions.sinh a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (eps₃₂ (Real.sinh a.val)))

FP32 sinh as an ≈[t] statement.

Informal: sinh(a.val) ≈[absOnly (eps₃₂(sinh(a.val)))] (sinh a).val.

theorem TorchLean.Floats.FP32.cosh_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (Real.cosh a.val) (MathFunctions.cosh a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (eps₃₂ (Real.cosh a.val)))

FP32 cosh as an ≈[t] statement.

Informal: cosh(a.val) ≈[absOnly (eps₃₂(cosh(a.val)))] (cosh a).val.

theorem TorchLean.Floats.FP32.sqrt_approxR (a : FP32) : Proofs.RuntimeApprox.approxR (√a.val) (MathFunctions.sqrt a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (eps₃₂ √a.val))

FP32 sqrt as an ≈[t] statement.

Informal: sqrt(a.val) ≈[absOnly (eps₃₂(sqrt(a.val)))] (sqrt a).val.

theorem TorchLean.Floats.FP32.abs_approxR (a : FP32) : Proofs.RuntimeApprox.approxR |a.val| (MathFunctions.abs a).val (Proofs.RuntimeApprox.ApproxTol.absOnly (eps₃₂ |a.val|))

FP32 abs as an ≈[t] statement.

Informal: |a.val| ≈[absOnly (eps₃₂(|a.val|))] (abs a).val.

Examples (how this looks in practice)