RFC: MePo premise selection — candidate-side symbol sets should match the goal side (instance/proof asymmetry)

Proposal

MePo premise selection scores each candidate by symbol overlap with the goal, but the two sides use
different walks:

• Goal side — MVarId.getRelevantConstants, which skips instance-implicit arguments
  and proofs (src/Lean/LibrarySuggestions/Basic.lean).
• Candidate side — ci.type.getUsedConstantsAsSet (src/Lean/LibrarySuggestions/MePo.lean), which keeps them.

Instance/proof symbols can therefore appear in a candidate's set but never in the goal's, inflating the
irrelevant term R' in the score M / (M + R') and capping the score of candidates that are a perfect match
modulo instances. The candidate side is also inconsistent with the rarity weights, since
symbolFrequencyMap is itself built from foldRelevantConstants (instances already excluded).

Reproduction (core-only, runs on the playground with Lean nightly)

See here for an example. Note that Nat.add_comm is a perfect match for n m : Nat ⊢ n + m = m + n, but scores 0.6 = 3/(3+2): its candidate symbol set carries instHAdd and instAddNat, which the goal side never produces, so they count only against it.

Proposed direction

Compute candidate symbol sets with the same relevantConstantsAsSet walk as the goal side. Doing it live
per query is too slow at scale, so persist each theorem's relevant-constant set in a persistent env
extension at module-export time — mirroring the existing symbolFrequencyExt.

Note that if we save these sets we can derive symbol frequency from them so we could unify the two. However, this is of course heavier than just storing the frequencies. (see below)

Cost / open questions (the reason this is an RFC)

1. stage0 change. If I understand correctly, to cover the whole stdlib the extension must be builtin in the bootstrapping compiler, so this requires an update-stage0. Is that right?
2. olean size. Preliminary local measurement (core, ~24.7k theorems): the per-theorem sets add ~6.4 MB to
   core oleans (~0.2% of total). The frequency map it subsumes is ~0.1–0.7 MB. Would this added weight be acceptable?

I can open a PR once the I get some confirmation that the proposed direction is sound. Finally, note that this current issue should be addressed before #13749. We need to have the correct set of "same-score-suggestions" before we can refine it and benchmark optimizations.

Start with src/Lean/LibrarySuggestions/Basic.lean and src/Lean/LibrarySuggestions/MePo.lean, comparing getRelevantConstants with getUsedConstantsAsSet and the existing symbolFrequencyExt path. Investigate the stage0 and OLean-size questions, then validate the candidate scores and core measurements against the linked reproduction. Done means the RFC's storage and export approach is confirmed or revised with evidence before implementation.