RealSemantics

Finite-only real semantics for IEEE32Exec.

We interpret a float32 bit-pattern as a real number by decoding its exact dyadic payload (-1)^sign * mant * 2^exp and then mapping to ℝ.

The executable kernel has NaN/Inf payloads; these do not have a real interpretation. We therefore provide:

• toReal? : IEEE32Exec → Option ℝ, returning none for NaN/Inf,
• toReal : IEEE32Exec → ℝ, a totalized version mapping none to 0.

Most theorems should be read under finiteness hypotheses and use toReal? (or lemmas that assume toDyadic? x = some …).

noncomputable def TorchLean.Floats.IEEE754.IEEE32Exec.toReal? (x : IEEE32Exec) : Option ℝ

Real interpretation for finite values (undefined for NaN/Inf).

noncomputable def TorchLean.Floats.IEEE754.IEEE32Exec.toReal (x : IEEE32Exec) : ℝ

Total real interpretation (maps NaN/Inf to 0; use toReal? for proofs).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_eq (x : IEEE32Exec) : x.toReal? = match x.toDyadic? with | some d => some (dyadicToReal d) | none => none

Unfolding lemma for toReal?.

This lemma is intentionally not [simp]: rewriting toReal? x into a match on toDyadic? x is usually not the best first step.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_of_toDyadic?_some {x : IEEE32Exec} {d : Dyadic} (hx : x.toDyadic? = some d) : x.toReal? = some (dyadicToReal d)

If toDyadic? x = some d, then toReal? x = some (dyadicToReal d).

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_of_toDyadic?_none {x : IEEE32Exec} (hx : x.toDyadic? = none) : x.toReal? = none

If toDyadic? x = none, then toReal? x = none.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_eq (x : IEEE32Exec) : x.toReal = match x.toDyadic? with | some d => dyadicToReal d | none => 0

Unfolding lemma for toReal in terms of toDyadic?.

This is the form that is most convenient in algebraic proofs: it avoids an intermediate Option.