perf: make environment extension replay proportional to the number of new entries

This PR makes the cost of realizing a constant (e.g. the equation lemmas needed by `simp only [f]`) independent of the size of the current file. Previously, files with many such realizations slowed down quadratically: on a file with 4,000 definition/theorem pairs elaboration time drops from 99 s to 32 s, and the time per pair is now constant.

Every `realizeConst` replays the extension changes it made onto the kernel environment, and all replays of a file run serially on the `checked` task chain. Several `replay?` implementations computed the new entries with `newState.take (newState.length - oldState.length)`, which walks all entries the extension accumulated in the file, and `LCNF.PhaseExt.replayFn` folded over the whole map of compiled declarations. The new `takeNewEntriesRev`/`takeNewEntries` helpers find the old list inside the new one by pointer equality, since entries are only ever consed onto it, and fall back to the length computation otherwise. `AbstractDeclExtState` now also records its keys in insertion order so the LCNF declaration and signature extensions replay only the new keys.

The new benchmark `tests/elab_bench/realizations.lean` measures this scenario.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QvNV36NuY94c36fRECjLFK
10 files changed