RL Float32 Semantics (IEEE32Exec)

TorchLean provides multiple “views” of float32:

• ExecFloat.Binary 8 23: executable, bit-level IEEE-754 binary32 (can run inside Lean),
• FP32: proof-oriented “round-on-$\mathbb R$” float32 model (finite-only).

The IEEE32Exec bridge files prove that, on the finite path, executable float32 arithmetic refines the standard mathematical model: compute the real operation and round to float32 at each primitive operation.

This module packages that theorem pattern for one of the most common RL formulas: the one-step discounted backup and TD residual used by TD learning, value iteration, and advantage estimation.

Practical takeaway:

If your runtime code checks that the relevant IEEE32Exec intermediates are finite (no NaN/Inf), then you can immediately “upgrade” that checked fact into a clean FP32-style real-rounding semantics for reasoning and error analysis.

References:

• IEEE 754-2019 (binary32 arithmetic): https://doi.org/10.1109/IEEESTD.2019.8766229
• Goldberg, “What Every Computer Scientist Should Know About Floating-Point Arithmetic” (1991): https://doi.org/10.1145/103162.103163
• Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed., discounted backups and TD learning): http://incompleteideas.net/book/the-book-2nd.html

theorem Proofs.RL.Float32Exec.toReal_discountedBackup_eq_fp32Round_chain_of_isFinite (reward gamma bootstrap : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal_discountedBackup_eq_fp32Round_chain_of_isFinite._proof_1 toReal_discountedBackup_eq_fp32Round_chain_of_isFinite._proof_2 toReal_discountedBackup_eq_fp32Round_chain_of_isFinite._proof_3 toReal_discountedBackup_eq_fp32Round_chain_of_isFinite._proof_4) (done : Bool) (h₁ : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.mul gamma (Spec.RL.continueMask done)) = true) (h₂ : FloatLib.Floats.ExecFloat.Binary.isFinite ((FloatLib.Floats.ExecFloat.mul gamma (Spec.RL.continueMask done)).mul bootstrap) = true) (h₃ : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.add reward ((FloatLib.Floats.ExecFloat.mul gamma (Spec.RL.continueMask done)).mul bootstrap)) = true) : (FloatLib.Floats.ExecFloat.Binary.toModel (Spec.RL.discountedBackup reward gamma bootstrap done)).toReal = TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel reward).toReal + TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round (TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel gamma).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel (Spec.RL.continueMask done)).toReal) * (FloatLib.Floats.ExecFloat.Binary.toModel bootstrap).toReal))

Refinement theorem for the RL one-step discounted backup in executable float32 semantics.

Assuming the relevant IEEE32Exec intermediates are finite, the decoded real value of the backup agrees with the standard “real op + round-to-float32” model (fp32Round) at each primitive op.

This is a useful building block for connecting executable RL code (IEEE32Exec) to textbook-style reasoning and error bounds phrased over ℝ + rounding.

theorem Proofs.RL.Float32Exec.toReal_tdResidual_eq_fp32Round_chain_of_isFinite (value reward gamma nextValue : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal_discountedBackup_eq_fp32Round_chain_of_isFinite._proof_1 toReal_discountedBackup_eq_fp32Round_chain_of_isFinite._proof_2 toReal_discountedBackup_eq_fp32Round_chain_of_isFinite._proof_3 toReal_discountedBackup_eq_fp32Round_chain_of_isFinite._proof_4) (done : Bool) (h₁ : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.mul gamma (Spec.RL.continueMask done)) = true) (h₂ : FloatLib.Floats.ExecFloat.Binary.isFinite ((FloatLib.Floats.ExecFloat.mul gamma (Spec.RL.continueMask done)).mul nextValue) = true) (h₃ : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.add reward ((FloatLib.Floats.ExecFloat.mul gamma (Spec.RL.continueMask done)).mul nextValue)) = true) (hval : FloatLib.Floats.ExecFloat.Binary.isFinite value = true) (hsub : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.sub (Spec.RL.discountedBackup reward gamma nextValue done) value) = true) : (FloatLib.Floats.ExecFloat.Binary.toModel (Spec.RL.tdResidual value reward gamma nextValue done)).toReal = TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round (TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel reward).toReal + TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round (TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel gamma).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel (Spec.RL.continueMask done)).toReal) * (FloatLib.Floats.ExecFloat.Binary.toModel nextValue).toReal)) - (FloatLib.Floats.ExecFloat.Binary.toModel value).toReal)

Refinement theorem for the TD residual / Bellman error in executable float32 semantics.

Formula: r + γ * (1-done) * nextValue - value.

Assuming the relevant IEEE32Exec intermediates are finite, the decoded real value of the TD residual agrees with the standard “real op + round-to-float32” model (fp32Round) at each primitive operation.