Komorebi Lean source runner

Install Python 3.11+, Git, and Elan from https://lean-lang.org/install/.
Unzip this bundle, open a terminal in its folder, and run:

  python run_lean.py --list
  python run_lean.py --source "PATH_FROM_THE_LIST" --output ../my-lean-run

Use a new output directory for each run. First runs download the pinned Lean
toolchain and Mathlib cache and can take several minutes and gigabytes of disk.
The runner executes native Lean, including the source's commands. Use it on
source you intend to run. Nothing executes just by viewing the website.

RUN_INPUTS.json records every staged source/configuration hash. RESULT.json and
per-step logs distinguish setup failures, timeouts, compiler failures, warnings,
and a clean compiler exit. A sorry warning is not a finished proof. No axiom or
whole-paper audit is performed and collection coverage labels do not change.

Retained projects keep their own toolchain and lockfile. Files without a Lake
project use a labelled reconstructed workspace: local imports are resolved to
the closest source edition inside the same work, distinct ties are rejected, and the
exact source bytes are copied into module paths. The overlay's pinned Lean and
Mathlib environment comes from the retained Paper V setup. It is an experiment
in that environment, not a claim to have recovered the original setup.

The bundle includes the retained Lean sources selected by the reading editions, plus
source/configuration inputs for their Lake projects. Compiled objects, package
caches, historical result logs and binary publication archives are omitted. Source/license paths and
checksums are listed in CATALOG.json. Keep this bundle with a run's records.
