feat: Float.Model

[TwoFX]

This PR adds types Float.Model and Float32.Model which will serve as logical models for the Float and Float32 types.

This PR contains just the implementation; we don't actually set it as the logical model yet. This will happen in a follow-up PR.

Further documentation will follow. For now, just the following information: the logical model will never support all of the operations that the native Float type supports. In this PR, we support the following operations: add, sub, mul, div, sqrt, abs, neg, isNaN, isInf, isFinite, le, lt, beq, ofInt, ofNat, ofIntX, ofUIntX, toIntX, toUIntX. Additional operations might follow in the future.

Extensive testing infrastructure is in place validating the model implementation against the native one using difficult test cases generated using Berkeley TestFloat and UCBTest.

[TwoFX]

Out of date comment

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 99683cc4dbbf60324235b721c81e0bd8ca4c3b69 --onto 4792cd22887c8b529a351f6563b693426ff2a8f8. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-16 18:26:33)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 99683cc4dbbf60324235b721c81e0bd8ca4c3b69 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-16 18:26:34)