FP32 Runtime-Approximation Bridge #
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
$$ |\mathrm{approx}-\mathrm{exact}| \le \varepsilon_{32}(\mathrm{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 meansx ≈[absOnly eps] yis exactly the usual bound $|y-x|\le\varepsilon$ (seeapproxR_absOnly_iff). This matches the shape of ourFP32theorems.The
FP32“epsilon” is value-dependent: $\varepsilon=\operatorname{ulp}(\mathrm{exact})/2=\varepsilon_{32}(\mathrm{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_leturns a plainabs (y - x) ≤ epsinequality into anapproxR.eps32_nonnegis the nonnegativity proof we need to useapproxR_absOnly_iff.
They are private because they are only used by this file's approximation bridge.
Arithmetic (one real op + one rounding step) #
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.
Informally, $\operatorname{val}(a)+\operatorname{val}(b) \approx_{\operatorname{absOnly}(\varepsilon_{32}(\operatorname{val}(a)+\operatorname{val}(b)))} \operatorname{val}(a+b)$.
FP32 subtraction, stated as an ≈[t] fact with t = absOnly (eps₃₂(exact)).
Informally, $\operatorname{val}(a)-\operatorname{val}(b) \approx_{\operatorname{absOnly}(\varepsilon_{32}(\operatorname{val}(a)-\operatorname{val}(b)))} \operatorname{val}(a-b)$.
FP32 multiplication, stated as an ≈[t] fact with t = absOnly (eps₃₂(exact)).
Informally, $\operatorname{val}(a)\operatorname{val}(b) \approx_{\operatorname{absOnly}(\varepsilon_{32}(\operatorname{val}(a)\operatorname{val}(b)))} \operatorname{val}(ab)$.
FP32 division, stated as an ≈[t] fact with t = absOnly (eps₃₂(exact)).
Informally, $\frac{\operatorname{val}(a)}{\operatorname{val}(b)} \approx_{\operatorname{absOnly}(\varepsilon_{32}(\operatorname{val}(a)/\operatorname{val}(b)))} \operatorname{val}(a/b)$.
Transcendentals (real function + rounding) #
FP32 exp is Real.exp followed by rounding; this is the result as an ≈[t] statement.
Informally, $\exp(\operatorname{val}(a)) \approx_{\operatorname{absOnly}(\varepsilon_{32}(\exp(\operatorname{val}(a))))} \operatorname{val}(\exp a)$.
FP32 tanh as an ≈[t] statement.
Informally, $\tanh(\operatorname{val}(a)) \approx_{\operatorname{absOnly}(\varepsilon_{32}(\tanh(\operatorname{val}(a))))} \operatorname{val}(\tanh a)$.
FP32 log as an ≈[t] statement (using Real.log as the exact reference).
Informally, $\log(\operatorname{val}(a)) \approx_{\operatorname{absOnly}(\varepsilon_{32}(\log(\operatorname{val}(a))))} \operatorname{val}(\log a)$.
FP32 cos as an ≈[t] statement.
Informally, $\cos(\operatorname{val}(a)) \approx_{\operatorname{absOnly}(\varepsilon_{32}(\cos(\operatorname{val}(a))))} \operatorname{val}(\cos a)$.
FP32 sin as an ≈[t] statement.
Informally, $\sin(\operatorname{val}(a)) \approx_{\operatorname{absOnly}(\varepsilon_{32}(\sin(\operatorname{val}(a))))} \operatorname{val}(\sin a)$.
FP32 sinh as an ≈[t] statement.
Informally, $\sinh(\operatorname{val}(a)) \approx_{\operatorname{absOnly}(\varepsilon_{32}(\sinh(\operatorname{val}(a))))} \operatorname{val}(\sinh a)$.
FP32 cosh as an ≈[t] statement.
Informally, $\cosh(\operatorname{val}(a)) \approx_{\operatorname{absOnly}(\varepsilon_{32}(\cosh(\operatorname{val}(a))))} \operatorname{val}(\cosh a)$.
FP32 sqrt as an ≈[t] statement.
Informally, $\sqrt{\operatorname{val}(a)} \approx_{\operatorname{absOnly}(\varepsilon_{32}(\sqrt{\operatorname{val}(a)}))} \operatorname{val}(\sqrt a)$.
FP32 abs as an ≈[t] statement.
Informally, $|\operatorname{val}(a)| \approx_{\operatorname{absOnly}(\varepsilon_{32}(|\operatorname{val}(a)|))} \operatorname{val}(|a|)$.