# Lean proof-check of one helper declaration

| | |
|---|---|
| Source commit | `048bb245b60abce79f1a2d0c82336ff8508ec752` |
| Module | `SpectreFinite.RadiusFiveRoot8Step1Chunk8_2Slice3` (`src/SpectreFinite/RadiusFiveRoot8Step1Chunk8_2Slice3.lean`, sha256 `19dbe58a…5a45`) |
| Declaration | `SpectreFinite.HexSearch.RadiusFive.root8Node0Step1Chunk8_2_slice3_checked` |
| Toolchain | `leanprover/lean4:v4.35.0-rc2`, from the `lean-toolchain` file. Official release tarball sha256 `b67d0e0b…a049`, which matches the digest GitHub publishes for the release asset. `lean --version` reports commit `11acb17ec6b07a8f9e9173e6845197929540936b`. |
| Dependency pins | `lake-manifest.json` (sha256 `ad06e9c9…3110`), Mathlib `065356127b1dc0016f66b7283ce0ce2c4055aa55`, `lakefile.lean` (sha256 `93980e47…78d9`). All are unchanged. |
| **Result for this helper** | **PASS.** Lean elaborated and kernel-checked the declaration (exit status 0). Its axioms are `[propext, Classical.choice, Quot.sound]`. |

The full hashes, commands and Lean output are in `evidence.txt` and `receipt.json`. Both files were written by `replay.sh` during the run. They were not edited by hand.

## What was checked

`replay.sh` runs these steps:

1. **Pins.** It refuses to run unless `src/`, `lean-toolchain`, `lakefile.lean` and `lake-manifest.json` are byte-identical to the pinned commit (`git diff --quiet <commit> -- …`) and there are no untracked files under `src/`. It also checks that the toolchain string and the Mathlib revision match the pins. Nothing in the repository is modified.
2. **Toolchain.** It downloads the official v4.35.0-rc2 release and verifies its sha256. Alternatively, `LEAN_HOME` can point at an existing install. In both cases the version string and git hash are verified.
3. **Compilation.** It computes the transitive import closure of the module from the source headers. The closure is **219 project modules plus Lean core `Init`**. No Mathlib or other Lake package is imported, so Mathlib is pinned but never loaded. Each of the 219 modules is compiled from source in dependency order with
   `LEAN_PATH=<build> lean -R src -o <build>/M.olean -i <build>/M.ilean -j1 -DElab.async=false src/M.lean`.
   The flags are the library's `moreLeanArgs`. All 219 exited with status 0. Compiling the target module also runs the source's own `#print axioms`.
4. **Audit.** It elaborates a generated file, `LeanProofUnitAudit.lean`, which is reproduced in full in the evidence. The file:
   - (a) restates the theorem's exact published statement in an `example` and proves it with the declaration;
   - (b) runs `#print axioms`;
   - (c) uses a `run_cmd` that checks the constant is a theorem, calls `Lean.collectAxioms`, and throws an error if any axiom is outside {`propext`, `Classical.choice`, `Quot.sound`}.
5. **Verdict.** PASS requires all of the following:
   - exit status 0 for every compile and for the audit;
   - the `AUDIT OK` line;
   - an axiom list that is a subset of the allowed set;
   - no `declaration uses sorry` warning and no `error:` in any module's Lean output.

   A run that exhausts the time budget is reported as INCONCLUSIVE, never PASS.

**Time limit.** Steps 3 and 4 run under a single `timeout 1200` (`CHECK_TIMEOUT` may be lowered but cannot exceed 1200). The recorded run took 15 s of wall time on a 32-core machine, with 32 parallel module compilations.

## Harness checks run

| Check | Outcome |
|---|---|
| Full run with toolchain download (the recorded run) | PASS, exit 0, 219 modules, axioms `[Classical.choice, Quot.sound, propext]` |
| `CHECK_TIMEOUT=3` | `timeout` exit status 124, so `INCONCLUSIVE`, harness exit 2 |
| `CHECK_TIMEOUT=1201` | refused, exit 3 |
| Audit block against a `sorry` theorem | `AUDIT_AXIOMS: [sorryAx]`, `AUDIT FAIL`, Lean exit 1 |
| Audit block against a theorem using a custom `axiom` | `AUDIT FAIL: disallowed axioms [myAx]`, Lean exit 1 |
| Audit block against a `def` | `AUDIT FAIL: … is not a theorem`, Lean exit 1 |
| Audit block against `rfl` theorem | `AUDIT OK`, exit 0 |

The negative tests were run in a scratch directory and are not part of the delivered evidence.

## Assumptions and deviations

- **Lake was not used.** The harness calls `lean` directly, so the Lake configuration was never elaborated. The 219 modules were compiled with the same Lean arguments the library declares, but not through the `PalomarAllDimensions` library target. Because the closure imports no Lake package, the result does not depend on the pinned packages.
- **Trust base.** The trusted components are the Lean v4.35.0-rc2 elaborator and kernel, plus the compiled `Init` that ships with the release. The declaration's proof uses `decide`, and Lean's kernel checked it. Its axiom report contains no `Lean.ofReduceBool` or `Lean.trustCompiler`, so no native-code evaluation is trusted.
- **Requirements.** The harness needs `bash`, `git`, `python3`, `curl`, `tar` with zstd, `sha256sum` and `timeout`. Network access is needed only for the toolchain download, which can be skipped by setting `LEAN_HOME`.
- **Mocks.** None were used.

## Explicitly NOT performed

These are separate, unperformed steps. Nothing in this unit claims them:

- **Final theorem comparison.** The comparator check of `PalomarAllDimensions.aperiodic_monotile_in_every_dimension` (Challenge against Solution) was **not run**.
- **Independent-kernel replay.** No replay with lean4checker or another external kernel was **performed**. The only checker was Lean's built-in kernel during elaboration.
- **Full build and preflight.** No Lake build of the whole library and no official Palomar preflight were run.

Checking this one helper (`root8Node0Step1Chunk8_2_slice3_checked`, one slice of a finite-table narrowing step) **does not complete or establish the all-dimensional theorem, and it is not a Palomar verification.**

## Reproduce

```sh
artifacts/lean-proof-unit/replay.sh            # writes evidence.txt and receipt.json next to the script
# optional: LEAN_HOME=/path/to/lean-4.35.0-rc2-linux JOBS=8 WORK_DIR=/tmp/x OUT_DIR=/tmp/out
```