RFC: parallel --fresh replay in leanchecker

leanchecker --fresh re-checks a whole import closure into a fresh environment through
the kernel — the trust-nothing mode. It's single-threaded (the README says so: "single
threaded, and may be much slower"), and on something like full import Mathlib that's
~18 min on a machine whose other cores sit idle.

I think the ordinary declarations in a --fresh replay could be checked in parallel
without weakening anything. Before anyone writes a real PR I'd like your read on two
things: whether it's worth having, and whether the approach below is sound.

The idea

--fresh trusts nothing in the .oleans — it's what you run when you don't trust the
build. It's also the slowest, and the only mode with no parallelism (the per-module
--num-workers path is parallel, but it checks against prebuilt imports, which is
weaker). So the strongest check is the one that doesn't use your cores.

Most of a replay is ordinary def/theorem/axiom/opaque declarations. Those could
be checked concurrently against a single growing environment: each worker runs
addDeclCore against the current committed env, and one committer thread commits the ones
that pass. Inductives/constructors/recursors/Quot and their postponed metadata checks
stay serial. Behind a jobs flag, with jobs=1 being today's path unchanged.

Why I think it stays sound

This is the part I'd most want a second pair of eyes on. The claim is that parallelism
only reorders the checking:

• addDeclCore stays the only thing that admits a declaration. You'd skip the re-check
  (addDeclWithoutChecking) only on a declaration that already passed addDeclCore
  against a snapshot holding all its deps — which is fine if checking is monotone (pass
  against a subset env ⇒ pass against a superset).
• No dependency graph decides correctness. If a declaration's deps aren't committed yet,
  addDeclCore fails with "unknown constant" and it's retried. The kernel is the
  dependency oracle; any ordering is just a scheduling hint.
• Anything still unchecked at the end gets re-checked serially, or the run fails.

I put together a rough prototype to sanity-check this, and on real closures up to full
Mathlib the result came out byte-identical to stock Environment.replay, and it still
rejected ill-typed / tampered-metadata / cyclic inputs. But I'd rather people who know the
kernel poke at the argument than take my word for it — especially the monotonicity step
and the "unknown constant means retry, not reject" bit.

Rough numbers

Just to show it's worth the trouble — 12-core machine, jobs=8, Mathlib v4.32.0, against
stock Environment.replay:

Roughly 3.7–4x. It won't get near core count — one growing env means one committer, and at
Mathlib scale memory bandwidth caps it — so it's a ~4x thing, not N×.

The usual four

• UX: faster --fresh on multi-core, opt-in; jobs=1 unchanged, no new trust.
• Who benefits: anyone re-checking a closure trust-nothing — CI on big libraries,
  security review, tools that re-verify against the kernel.
• Feedback: opening this here to gather it; I couldn't find an existing issue or PR
  for parallel --fresh.
• Maintenance: ~400 lines, additive — one new parallel section; reuses
  replayConstant / checkPostponed* unchanged, and jobs=1 is the current serial body
  pulled into a shared helper so the two paths can't drift.

Questions

• Is this worth having at all?
• Is a jobs flag on Environment.replay / leanchecker the right shape, or would you
  want it somewhere else?
• Anything in the soundness sketch that doesn't hold?

If the direction's welcome I'm happy to turn the prototype into a proper PR. It'd be
additive — a parallel path reusing the existing serial checks — and there'd be details to
settle: memory use (it's heavier), a sensible default jobs, and tests.

I designed and drafted this proposal together with AI, and I've reviewed and verified the
argument and the measurements myself.

Start with Environment.replay, leanchecker, and the existing replayConstant and checkPostponed* paths described in the proposal. Examine addDeclCore handling and the serial replay behavior first, then evaluate the prototype's byte-identical results and rejection tests. Done would require an agreed sound design, settled jobs and memory behavior, and coverage for parallel replay without changing jobs=1.