feat: symbol frequency extension

[kim-em]

This PR adds an environment extension for tracking the frequency of symbols in declaration signatures.

On the export of each module, we scan the new constants' types and generate a frequency map just for that module.

When the extension is imported, we do nothing.

When the extension is queried, we assemble the frequency maps for all imported modules into a single NameMap Nat, and cache that in an IO.Ref.

[kim-em]

!bench

[leanprover-radar]

Benchmark results for 6f9ffa1 against 3ce7d4e are in! @kim-em

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3ce7d4ef5c85db47439cf3a9d8adf280a9dda768 --onto efbbb0b230ce95653d25b59c83fd24a51a8bf363. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-23 03:20:32)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d5ca0c7032fe18e5bbdb19600075e01677bca659 --onto efbbb0b230ce95653d25b59c83fd24a51a8bf363. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-25 09:11:38)

[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 3ce7d4ef5c85db47439cf3a9d8adf280a9dda768 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-23 03:20:34)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase d5ca0c7032fe18e5bbdb19600075e01677bca659 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-25 09:11:39)

[leanprover-bot]

Here are the benchmark results for commit 6f9ffa1.
There were significant changes against commit 3ce7d4e:

  Benchmark                          Metric          Change
  ====================================================================
- Init size                          bytes .olean      1.3%
+ channel.lean                       boundedn_seq     -7.4%
+ riscv-ast.lean                     branch-misses    -1.6% (-429.9 σ)
- stdlib                             blocked           3.0%   (20.2 σ)
- stdlib size                        bytes .olean      1.2%
+ workspaceSymbols with new ranges   branches         -2.2% (-122.6 σ)
+ workspaceSymbols with new ranges   instructions     -3.0% (-124.7 σ)