perf: normalize universe parameters in the type class cache key (experiment, dropped) Unifies universe-parameter normalization with the free-variable normalization of the cache key: `normExpr` renames universe parameters to canonical positions `_snl.i` by first occurrence, threaded through the same `SynthNormClosure` memo as the free variables, with the value re-specialized on `reopen` via `instantiateLevelParams`. Universe parameters are rigid, so this is a bijective renaming and carries no assignability hazard, unlike the metavariable-key experiment. Sound across all 8259 Mathlib modules (0 regressions) and cheap once memoized (+1.9% on `Different`, down from +18.9% for an earlier non-memoized post-pass). Dropped because it recovers nothing: universe parameters that differ only by renaming are essentially absent from type class queries during elaboration (0 on `Different`), where universes are almost always metavariables rather than parameters. An earlier apparent -11% win on `GroupTheory/FreeAbelianGroup` was a measurement artifact of a handicapped baseline that refused to cache parameter-carrying values; corrected, every file measured is +1 to +2.5% pure overhead. Kept on the `param-norm-experiment` bookmark in case a parameter-heavy workload ever makes it worthwhile. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.