5. Floating Point and Native Boundaries
This chapter is the numeric handoff between the semantic story and the verification story. A
TorchLean claim may talk about real specifications, finite rounded real FP32 proofs, executable
IEEE32Exec bit behavior, Lean runtime Float32, CUDA kernels, or an external verifier artifact.
Those are different objects. The point of this chapter is to name each object, show the Lean
declarations that represent it, and explain which bridge theorem or assumption is needed before a
claim can move from one layer to another.
Read it in this order: float semantics first, then the citation map, then CUDA/native execution,
then external tools, then the FP32 soundness notes that the verification chapter uses.