Add a lean_kernel option to skip the builtin kernel replay

[mt0-svg]

Comparator always replays the solution in the Lean kernel (runBuiltinKernel in verifyMatch), also when external kernels are configured. For a large development this replay is a second full kernel check of code that the Lean kernel already checked during lake build, and it can dominate the run time. On one of our packages, on a 4 core GitHub runner, nanoda (4 threads) replays the export in about 57 minutes and the builtin kernel in about 3 hours 6 minutes.

This PR adds an optional config field lean_kernel. The default is true, so existing configs behave exactly as before. With "lean_kernel": false, comparator skips runBuiltinKernel and leaves the replay to the configured external kernels. The challenge build, the export, the statement comparison, the axiom check and the external kernels are unchanged.

A config with "lean_kernel": false and no external kernel is rejected at startup, so a solution can never pass without a kernel replay. The quotient check done after runBuiltinKernel is skipped with it; nanoda checks the Quot declarations itself.

The README gets one paragraph under "Checking with Additional Kernels".

Tests, in the existing tests/projects layout:

• lean_kernel_off_nanoda: correct solution, nanoda only, accepted.
• lean_kernel_off_mismatch: a different statement under the challenge name, rejected.
• lean_kernel_off_unchecked: a theorem added with debug.skipKernelTC whose value proves 0 = 0 while its type is 0 = 1, rejected by nanoda.
• lean_kernel_off_no_kernel: lean_kernel false with no external kernel, refused at startup.

The full suite passes (24 of 24) with nanoda_bin on PATH, as simple_multi_nanoda already requires.

Tested on d03acab (Lean v4.34.0); the patch applies cleanly to the current main.