mepo: score function over-rewards tiny generic theorems

For a goal like a + b = b + a : Int, mepoSelector ranks Int.add_comm around position 36 (and around 67 without applying the wasOriginallyTheorem filter that the other selectors in this directory already use). The top 30 are score-1.0 entries like Eq.symm, Eq.trans, proof_irrel, congrArg, funext, Eq.subst, congr.

These are real theorems, so the wasOriginallyTheorem filter doesn't help them. They score 1.0 because

score = M / (M + R')
  where  R  = relevant ∩ candidate
         R' = |candidate \ relevant|
         M  = Σ weight(n)  for n in R

A one-symbol theorem like Eq.symm (symbol set {Eq}) whose lone symbol is in relevant scores M/M = 1 no matter what M is, since R' = 0. The formula rewards fraction of overlap, not amount.

Two candidate fixes I'd like opinions on, both of which compose with the lexicographic-by-(iteration, score) ordering we likely want anyway (cf. lean#13747 and Xavier's report):

(1) Additive damping in the denominator. Replace M / (M + R') with M / (M + R' + γ) for some γ > 0. A theorem with M = 1 then scores 1/(1+γ) instead of 1, while one with M = 8 scores 8/(8+γ) — still close to 1. One tunable knob. Changes threshold semantics (every score drops), so the p = 0.6 schedule would need retuning.

(2) Tiebreak within an iteration by |R|. Keep the score formula and threshold. Sort within each iteration by (score desc, |R| desc) instead of just score desc. A theorem matching 8 of the goal's symbols then ranks above one matching 1, even when both score 1.0.

(1) changes which premises clear the threshold. (2) only changes their order — never changes the accepted set.

cc @xgenereux — opening this rather than picking one because either direction wants benchmarks before tuning, and I'd like your read first.

🤖 Prepared with Claude Code

Start by locating mepoSelector and comparing its scoring, filtering, and ordering with the other selectors in that directory; review lean#13747 and Xavier's report for the intended ordering. Add or run benchmarks for both damping and |R| tie-breaking, and document which approach preserves the desired threshold and ranking behavior.