perf: shorten critical build path around String.Basic

[TwoFX]

This PR cuts some edges from the import graph.

Specifically:

• TreeMap and HashMap no longer depend on String, so now the expensive things are all in parallel instead of partially in sequence
• Omega no longer relies on List lemmas
• The section of the import graph between Init.Omega and Init.Data.Bitvec.Lemmas is cleaned up a bit

[TwoFX]

!bench

[leanprover-bot]

Here are the benchmark results for commit 8b71d99.
There were significant changes against commit 4338a8b:

  Benchmark   Metric       Change
  ===========================================
+ stdlib      wall-clock    -2.1% (-1573.5 σ)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-09-29 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. (2025-09-29 12:50:34)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-29 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. (2025-09-29 12:50:35)

[TwoFX]

!bench

[TwoFX]

!bench

[leanprover-bot]

Here are the benchmark results for commit 53edc0a.
There were significant changes against commit 4338a8b:

  Benchmark      Metric                    Change
  ==========================================================
+ channel.lean   unbounded_seq              -5.9%
- stdlib         process pre-definitions     2.4% (1064.5 σ)
+ stdlib         wall-clock                 -2.7% (-193.4 σ)

[leanprover-bot]

Here are the benchmark results for commit 77c870f.
The entire run failed.
Found no significant differences.

[TwoFX]

!bench

[leanprover-bot]

Here are the benchmark results for commit 9ee59d8.
There were significant changes against commit 4338a8b:

  Benchmark      Metric                        Change
  =============================================================
- simp_local     branch-misses                  11.2%  (20.8 σ)
- stdlib         blocked (unaccounted)           5.4%  (27.0 σ)
- stdlib         compilation (LCNF base)         2.8%  (33.4 σ)
- stdlib         compilation (LCNF mono)         5.4%  (21.2 σ)
+ stdlib         longest build path             -7.1% (-39.9 σ)
+ stdlib         longest rebuild path           -7.7% (-28.2 σ)
+ stdlib         number of imported consts      -1.1%
- stdlib         process pre-definitions         9.1%  (61.9 σ)
- stdlib         type checking                   5.3%  (30.0 σ)
+ stdlib         wall-clock                     -7.4% (-22.3 σ)
+ treemap.lean   insertRandomMissEmptyShared    -1.7% (-25.8 σ)

[TwoFX]

!bench

[TwoFX]

!bench

[leanprover-bot]

Here are the benchmark results for commit c26586c.
There were significant changes against commit 4338a8b:

  Benchmark       Metric                       Change
  ==============================================================
+ hashmap.lean    eraseInsert                   -5.9% (-434.6 σ)
+ hashmap.lean    iterate                      -11.8%  (-45.7 σ)
+ phashmap.lean   insertMissEmpty               -5.3%  (-21.4 σ)
- stdlib          attribute application          6.1%   (21.6 σ)
- stdlib          grind dsimp                    4.1%   (78.3 σ)
+ stdlib          longest build path            -9.5%  (-44.4 σ)
+ stdlib          longest rebuild path          -9.2%
+ stdlib          number of imported bytes      -2.4%
+ stdlib          number of imported consts     -2.8%
+ stdlib          number of imported entries    -1.9%
+ stdlib          task-clock                    -8.8%  (-94.3 σ)
+ stdlib          wall-clock                    -9.0%  (-35.5 σ)

[leanprover-bot]

Here are the benchmark results for commit 464939a.
There were significant changes against commit 4338a8b:

  Benchmark                            Metric                       Change
  ===================================================================================
+ Std.Data.Internal.List.Associative   maxrss                        -4.7%  (-25.4 σ)
+ channel.lean                         boundedn_seq                  -7.2%
+ grind_ring_5.lean                    branch-misses                 -2.4%  (-52.3 σ)
+ riscv-ast.lean                       branch-misses                 -1.2% (-250.0 σ)
+ stdlib                               longest rebuild path          -8.6%  (-23.4 σ)
+ stdlib                               number of imported bytes      -2.4%
+ stdlib                               number of imported consts     -2.8%
+ stdlib                               number of imported entries    -1.9%
+ stdlib                               task-clock                    -8.6%  (-40.2 σ)
+ stdlib                               wall-clock                    -8.9%  (-25.5 σ)