I ran the replay harness on the pinned project and the check passed. Lean v4.35.0-rc2 compiled and kernel-checked SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_2_slice3_checked (exit 0). Its axioms are exactly [propext, Classical.choice, Quot.sound].

The four outputs are in artifacts/lean-proof-unit/ and are left untracked:

• replay.sh – the harness. It does this:
  • Pins: it refuses to run unless src/, lean-toolchain, lakefile.lean and lake-manifest.json are byte-identical to commit 048bb245…. It also checks the Mathlib revision.
  • Toolchain: it downloads the official v4.35.0-rc2 release and checks its sha256, which matches the digest GitHub publishes. It also confirms Lean's version and commit.
  • Compile: the module needs only 219 project modules plus Lean core, with no Mathlib, so it compiles those from source with the library's own flags (-j1 -DElab.async=false).
  • Audit: it confirms the declaration is a theorem with exactly the published statement, prints its axioms, and fails if any axiom is outside the allowed three.
  • Time limit: compiling and auditing share one 1200-second limit, and running out gives INCONCLUSIVE, never PASS.
• evidence.txt and receipt.json – written by the harness during the final run, not by hand. They hold the commands, Lean's output, exit statuses, every pin hash, and a per-module exit line for all 219 modules. The run took 15 seconds on 32 cores.
• report.md – results, assumptions, the self-tests, and a separate section on what was not done.

Self-tests (scratch only, not delivered):

• A 3-second time limit gave INCONCLUSIVE, and a limit above 1200 is refused.
• The audit rejected a theorem using sorry, one using a custom axiom, and a plain definition.
• A test also caught a bug, now fixed: this Lean version prints the sorry warning with backticks, which my first pattern didn't match.

Differences from the official route:

• The harness calls lean directly instead of Lake, so the Lake configuration and the full library build weren't run. The module imports no Lake packages, so the result doesn't depend on them.
• The final all-dimensional theorem comparison and an independent-kernel replay were not done. The report says this checked helper does not complete the all-dimensional theorem or Palomar verification.

I didn't create the stray entries in the repository root (.bashrc, .github, scripts and others). They are sandbox device stubs, and I left them alone. An empty .claude folder that the tooling made in the output directory has been removed.