feat: bundle the `lean4lean` external checker with release toolchains

This PR ships the `lean4lean` external checker in release toolchains, alongside `leanchecker`, so an independent kernel implementation is available out of the box.

A `lean4lean` build target fetches and builds it, pinned by `LEAN4LEAN_REV`. Like `leanchecker-paranoid` the target is not part of `ALL`, here because it fetches; release CI builds it explicitly. It drops the binary into the build tree, so the existing `bin/` install rule ships it.

It is built with the toolchain `lean4lean` itself pins, not with the toolchain being released, because it consumes the export format rather than `.olean`s: `bin/leanexport` writes an export file and `lean4lean --import` reads it, so none of the githash locking `CHECK_OLEAN_VERSION` applies to olean reads is involved, and the binary needs no rebuild per release. The build links `-linitialize_minimal` rather than initializing all of `Lean`, which takes the binary from 117 MB to 36 MB; that is sound only because the checker never elaborates Lean source, so it is applied here rather than asked of `lean4lean`, which must stay buildable against toolchains without `libinitialize_minimal.a`.

Building is not evidence of working, though. `lean4lean` models Lean's primitive definitions, so a revision predating a change to them still builds against its own toolchain but rejects code using those primitives. `tests/pkg/lean4lean` therefore exports `Init.Data.List.Basic` and checks it through `--import`, which replays into an empty environment and so re-adds every primitive; it skips when the binary was not built, so it costs ordinary test runs nothing. `tests/elab/lean4lean_primitives.lean` pins the definitional shapes an external checker matches on, so a change to them fails in the PR that makes it rather than at release time.

The build step runs on release builds only and deliberately hard-fails, so a checker that cannot check this Lean blocks the release rather than being shipped broken. Nightlies and ordinary CI are unaffected.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JPPJuXrRxwXgsWEAqM62dd