5. Floating Point and Native Boundaries🔗

Our graph equations use real numbers, but the program does not. This part starts with that mismatch and develops TorchLean's floating-point stack. The story begins with Flocq's influential separation of formats from rounding, continues through TorchLean's generic NeuralFloat theory, and ends with executable binary32 and native kernels.

1. 5.1. Floating-Point Semantics
2. 5.2. Tracking Numerical Error Through A Network
3. 5.3. From A Tensor Operation To A GPU Kernel
4. 5.4. Crossing Lean's Boundary
5. 5.5. Float32 Soundness