Add independent-kernel shadow smoke

[kim-em]

Summary

• add a manual, credential-free independent-kernel shadow smoke;
• pin the accepted public two_plus_two result and exact
  LeanEval/Mathlib/exporter/comparator/checker identities;
• build every component from source, strip credentials and Git metadata, run
  the standard sandbox probes, and invoke MathGraph through Comparator only
  after normal acceptance;
• upload strict source-free evidence without changing acceptance, Results,
  State, replay queues, releases, or the required checker set; and
• document that this is one compatibility point, not a corpus backtest,
  performance result, or checker-promotion decision.

MathGraph is the first shadow candidate because its pinned Arena result is
121/121 expected accepts, 66/66 expected rejects, and zero declines. It remains
experimental and is not promoted by this PR.

Current verification

Final review head: b8ec24aaad74a13211ac49618d8968a518cf0496.

• synchronized current main before independent review;
• local full suite: 289 tests passed with one expected optional-tool skip under Python warnings-as-errors;
• action-pin audit, Python byte-compilation, and diff checks pass;
• hosted CI run 32557185003 passes, including actionlint and all security/contract tests;
• hosted Worker-check run 32557185008 passes; promotion and both deployment jobs correctly skip;
• full local executable pipeline on LeanEval 21c6c021, Lean 4.33.0,
  Mathlib 6f1ef4e, exporter 15f6055, Comparator 19e111e, MathGraph
  3d7585c, and Arena 34f87c4;
• exact Rust pin rustc 1.95.0 (59807616e 2026-04-14) established by the
  executable smoke; and
• built-in Lean kernel and MathGraph both accepted the reviewed public source,
  with sandbox and environment-dump probes passing.

This workflow requires independent review before merge because it builds and
executes an external checker, even though it is manual, credential-free,
non-authoritative, and does not deploy from a pull request.

[kim-em]

Pre-review cleanup 33ac598 clears all Ruff findings in the newly added Python files (including the executable/shebang mismatch) without changing the smoke contract. Revalidation: 288 warning-enabled repository tests pass (1 environment-dependent age test skipped), focused 12/12 pass, Ruff zero findings, actionlint clean, action-pin audit clean, and diff check clean.

[kim-em]

Full executable pre-review smoke found and fixed a real toolchain mismatch. The pinned MathGraph commit’s locked graph contains stumpalo 0.5.1, whose declared minimum Rust is 1.95.0; the workflow’s previous exact 1.89.0 pin fails before compiling the candidate. Commit 9206d31 advances only this smoke to exact rustc 1.95.0 (59807616e 2026-04-14) and locks that version in the structural test.\n\nI then reproduced the complete pipeline locally from clean exact checkouts: lean4export 15f6055, comparator 19e111e, MathGraph 3d7585c, Arena 34f87c4, benchmark 21c6c021, public source a7cf16e, Lean 4.33/Mathlib 6f1ef4e. Rust 1.89 failed with the MSRV error; Rust 1.95 built the locked candidate (sokonanoda SHA-256 a77fc6cab698f938333c5030f07e4309a0e0ca77a391d2a71ea21032741af63d). Both sandbox probes passed, comparator built/exported Challenge and Solution, MathGraph accepted, Lean’s default kernel accepted, and the pipeline exited 0 in 21,864 ms. This is local compatibility evidence, not a substitute for the post-merge Ubuntu staging workflow.\n\nAll 288 repository tests (one age-tool skip), focused 12 tests, Ruff, Python bytecode, actionlint, pin scan, and diff checks pass. Fresh hosted PR CI is green: https://github.com/leanprover/lean-eval-submissions/actions/runs/32521208190.