Bridge lemmas between executable IEEE32 arithmetic and the FP32-facing API.

The submodules expose operation-level, rounding, and totality facts for verification code that uses binary32 semantics rather than Lean's host Float behavior.