feat: fix and expose Float.ofScientific

[TwoFX]

This PR completely rewrites the implementation of Float.ofScientific.

The new implementation passes all 5+ million tests from the parse-number-fxx-test-data suite. This comes at the expense of being significantly slower than the previous implementation. Unfortunately, based on my investigations, the old routine involving Float.scaleB seems difficult to salvage because it suffers from double-rounding issues, at least if the result turns out to be a subnormal. The algorithm described at https://www.exploringbinary.com/correct-decimal-to-floating-point-using-big-integers/ can deal with these problems, but it is also very slow.

The routine implemented here is as follows: we have a fast path if both the significant and the power of ten can be represented exactly; this should happen most of the time in normal usage. Otherwise, we call out to a model implementation on UnbundledFloat which manages to avoid the double-rounding issues. This is quite slow according to my measurements: the slowdown in this path is between 10x and 20x.

The new implementation can be executed in the kernel, though at the moment the slow path requires either a bump to the recursion depth or the use of decide +kernel.

This means that

example : 0.1 + 0.2 != 0.3 := rfl

works now.

The full parse-number-fxx-test-data suite is more than 200MB in size, so we do not include it here; instead, in CI we only test 10k tests from that suite, and the full suite can be run locally if desired.

Closes #13982.

[TwoFX]

!radar

[leanprover-radar]

Benchmark results for 9a21edb against 5822584 are in. No significant results found. @TwoFX

• ✅ build//instructions: -4.2M (-0.00%)

Small changes (1✅, 1🟥)

• 🟥 build/module/Init.Data.OfScientific//instructions: +208.0M (+32.75%) (reduced significance based on *//lines)
• ✅ build/module/Lean.Elab.BuiltinDo//instructions: -12.9M (-2.04%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-06-18 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-18 16:31:03)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-06-18 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-06-18 16:31:04)

[Rob23oba]

example : 0.1 + 0.2 = 0.3 := rfl
Hmm........ I sense an upside down "i" missing in that example