Bridges From Executable Binary32

This umbrella collects the refinement layers around IEEE32Exec: finite rounded-real semantics, total special-value semantics, expression-level composition, extended-real interpretation, and the explicit trust boundary to Lean's runtime Float32.