5. Floating Point and Native Boundaries
Neural network claims often move across numerical worlds. A model may be specified over the reals, executed in Float32, accelerated by CUDA, bounded by a verifier, and checked through an imported certificate. These worlds are connected, but they are not identical.
TorchLean separates them deliberately. Real-valued specs are used for clean mathematical
statements. FP32 gives a rounded-real proof model for error budgets. IEEE32Exec gives
executable binary32 behavior inside Lean, including special values. Native execution through Lean
Float32, CUDA, cuBLAS, cuFFT, Python, Julia, Arb, or external verifiers enters through explicit
producer/checker interfaces.
The goal is not to avoid practical numerical tools. The goal is to know exactly how their outputs support the claim being made.