5.2.1. Three Questions Before Citing A Result🔗

For a "floating-point universal approximation" claim, three concrete checks apply:

1. Is the theorem about reals, about a rounded real model, or about actual executable IEEE-754 bits?

2. What is the approximation target (a pointwise function, a direct image of a set, or an interval enclosure)?

3. If the theorem is meant to feed a verifier, what semantics is the verifier using?

TorchLean keeps these cases separate in code:

• FP32 is the rounded real model used in proofs.

• IEEE32Exec is the executable binary32 kernel.

• NN.IR.Graph is the shared "this is the computation" object used by execution and verification.

Two common citation chains are:

• real target function, classical approximation error, FP32 rounding model, then interval or LiRPA verification semantics;

• executable IEEE32Exec bits, then the FP32 proof model on the finite bridge path.

5.2.2. Definitions we use in this book🔗

• direct image: the exact output set f(B) of a network over an input region B.

• interval abstraction: a sound overapproximation of f(B) (a box, or a box plus affine forms).

• rounded target: the same computation after fixing a scalar semantics (reals vs FP32 vs IEEE bits).

• bridge theorem: a statement that connects an executable semantics to a proof semantics on a stated "finite path" (no NaN/Inf, no overflow, etc).

The same feed-forward architecture can therefore be discussed at several incompatible levels of precision. Papers and theorems should name the level explicitly so readers can tell whether the claim concerns real valued idealization, a float model used for proofs, executable IEEE-754 behavior, or a verifier's overapproximation of outputs.

5.2.3. Key References🔗

5.2.4. What TorchLean Can Cite Today🔗

TorchLean already has a chain checked by Lean that is more concrete than a paper sketch:

• a classical 1D ReLU universal-approximation theorem,

• a hinge-network variant of that theorem,

• and an FP32-flavored version with an explicit rounding bound.

import NN.MLTheory.Proofs.Approximation
import NN.MLTheory.Proofs.Approximation.Universal.UniversalApproximationIEEE32Exec

#check relu_universal_approximation_Icc
#check relu_universal_approximation_Icc_hinge
#check relu_universal_approximation_Icc_fp32

Read the three theorems as a staged chain:

• relu_universal_approximation_Icc states the classical real valued universal approximation result.

• relu_universal_approximation_Icc_hinge is a constructive hinge-network variant that exposes the piecewise-linear structure used in later proofs.

• relu_universal_approximation_Icc_fp32 layers TorchLean's FP32 rounding model on top of that approximation theorem, with an explicit rounding error budget.

Together they illustrate the pattern the rest of the numerics chapters follow: establish the real valued property, fix a scalar semantics, then package a compositional error or refinement lemma that links the two.

import NN.MLTheory.Proofs.Approximation.Universal.UniversalApproximationIEEE32Exec

#check relu_universal_approximation_Icc_ieee32exec_minimal
#check relu_universal_approximation_Icc_ieee32exec_threeTerm
#check relu_universal_approximation_Icc_ieee32exec_twoTerm

5.2.5. What A Full Paper Statement Still Has To Package🔗

The remaining work is concrete theorem packaging. A paper-ready theorem has to quantify over:

• the real target function or real network being approximated;

• the scalar semantics used by the executable model (FP32, IEEE32Exec, or a runtime bridge);

• the classical approximation error ε_appx;

• the finite precision or rounding error ε_fp32;

• the interval, CROWN/LiRPA, or certificate error term ε_verify, if the statement is verifier side;

• the bridge hypotheses: finite values, no overflow, fixed reduction order, and any runtime/native agreement assumptions.

Only after those pieces are explicit can the theorem state a combined bound such as:

\varepsilon_{\mathrm{total}} = \varepsilon_{\mathrm{appx}} + \varepsilon_{\mathrm{fp32}} + \varepsilon_{\mathrm{verify}}

That is where the verification and floating-point chapters should be cited together.

A typical citation bundle for this combined topic is:

• Floating-Point Semantics for FP32, IEEE32Exec, and bridge theorems;

• FP32 Soundness Notes for the rounding model used in proofs and its theorem names;

• Verification for the interval / LiRPA / certificate side;

• approximation proofs for the universal-approximation theorems themselves.

5.2.6. References🔗

• Hwang, Saad, et al. Floating-Point Neural Networks Are Provably Robust Universal Approximators. arXiv:2506.16065, CAV 2025. https://arxiv.org/abs/2506.16065

• Cybenko, G. Approximation by superpositions of a sigmoidal function. 1989.

• Hornik, Stinchcombe, and White. Multilayer feedforward networks are universal approximators. Neural Networks, 1989.

• Leshno et al. Multilayer feedforward networks with a nonpolynomial activation function can approximate any function. Neural Networks, 1993.

• Pinkus, A. Approximation theory of the MLP model in neural networks. Acta Numerica, 1999.

• Sakr et al. Analytical Guarantees on Numerical Precision of Deep Neural Networks. ICML 2017. PMLR page

• Gehr et al. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. 2018.

• Singh et al. An Abstract Domain for Certifying Neural Networks. POPL 2019.

• Goldberg, D. What Every Computer Scientist Should Know About Floating-Point Arithmetic. Oracle-hosted reprint

• Higham, N. Accuracy and Stability of Numerical Algorithms. SIAM book page

• IEEE Std 754-2019. Standard for Floating-Point Arithmetic. IEEE 754-2019

• ISO/IEC/IEEE 60559:2020. Floating-point arithmetic. ISO/IEC/IEEE 60559:2020

• Flocq project documentation. Flocq

• FloatSpec for Lean 4. FloatSpec

• Gappa, Certifying floating-point implementations using Gappa. Gappa paper

• CompCert commented development. CompCert