Approximation proofs

This entrypoint collects TorchLean's approximation-theory proof chapter. We separate the two main threads while keeping them importable together:

• constructive ReLU universal approximation over real semantics, with quantitative and finite-precision variants; and
• exact interval semantics for rounded binary32 targets.

Both threads expose the mathematical assumptions and numerical side conditions explicitly rather than burying them inside runtime behavior.