Universal-approximation proofs

This entrypoint collects the constructive ReLU approximation results:

• one-dimensional constructive ReLU approximation by hinge sums;
• quantitative width/rate refinements;
• finite-precision lifts through FP32 and executable ExecFloat.Binary 8 23 semantics; and
• an n-dimensional Stone-Weierstrass bridge through coordinate polynomials.

The results connect the exact real-valued construction to TorchLean's spec-level MLP and executable binary32 arithmetic.

References:

• Cybenko, "Approximation by superpositions of a sigmoidal function", 1989.
• Leshno, Lin, Pinkus, and Schocken, "Multilayer feedforward networks with a nonpolynomial activation function can approximate any function", 1993.
• Pinkus, Approximation Theory of the MLP Model in Neural Networks, 1999.
• Yarotsky, "Error bounds for approximations with deep ReLU networks", 2017.