Evidence release
This page identifies the exact files behind the paper’s computer-assisted claims: the PDF, the Lean formalisation, the certificate data and their checkers, with checksums, the commands that check them, and an archived copy. The site itself may change after submission; the release below does not.
Status: Frozen. Release v1.1 is tagged and archived; the site may change later, this release does not.
Identity
| Release | v1.1 (2026-11-01) |
| Tag | v1.1 |
| Paper | Monotone Local Search with Sample-Dependent Running Times, manuscript of 2026-11-01 |
| Research repository commit | e66f22a4e23a1d9c45b4688a35e5a73b5d8f7953 |
| Site commit | the commit of tag v1.1 |
| arXiv | |
| Archived copy | Zenodo, DOI 10.5281/zenodo.23851002 |
The PDF, the Lean sources, the certificate data, the checkers and the checksums below all come from the same revision.
Release v1.1 (2026-11-01) replaces release v1 (2026-10-31) before the paper’s arXiv announcement (as arXiv:2611.01774, 2026-11-03). It corrects errors found by audits of v1: the Max Leaf Spanning Tree claim of Corollary 8.5 now holds for \(n\ge3\) (for \(n=2\) the reduction gives one leaf too few; Theorem 8.1 treats \(n\le2\) directly), Appendix F’s summary of the Lean results now matches them, and the site’s coverage notes, Appendix D numbers and build descriptions are corrected. The \(n\le2\) sentence of Lemma 5.1 is now proved in Lean (CDS.maxLeaf_small). The certificates and their checkers are unchanged. Release v1 stays available, frozen, under /v/v1/ and on Zenodo.
Files
| File | Contents |
|---|---|
sample-dependent-mls.pdf |
the paper |
sample-dependent-mls-source.tar.gz |
the LaTeX source of the paper as submitted to arXiv (main.tex, main.bbl); the full arXiv upload with the ancillary files as anc/ is on the archived copy |
sample-dependent-mls-check.zip |
everything needed for checking: the Lean project and the ancillary files, with a README |
sample-dependent-mls-lean.zip |
the Lean project alone |
manifest.json |
each computer-assisted statement of the paper with its checker files and its Lean declarations |
axioms.txt |
the axiom audit of the Lean declarations linked from the paper in the project’s default target (the 14 of the RSC data target are in evidence/axioms-data.txt) |
SHA256SUMS |
SHA-256 checksums of the files above |
Inside the checking bundle, ancillary/SHA256SUMS lists the checksums of every certificate, checker and recorded output, and lean/lake-manifest.json pins every Lean dependency. To check downloads: sha256sum -c --ignore-missing SHA256SUMS in the folder that holds them (on macOS, shasum -a 256 -c --ignore-missing SHA256SUMS). --ignore-missing skips the files you did not download; on the site, the PDF and the LaTeX source are served from the paper’s folder, not from downloads/.
Checking the certificates
The script ancillary/verify_all.sh checks the ancillary checksums, runs every checker that a proof depends on, and compares each output with the author’s recorded output. Its two modes certify different things:
- Quick mode checks every certificate that a proof depends on except the RSC antinorm certificate (Proposition D.5.23). “All checks passed” after the quick mode does not say that the RSC certificate was verified.
- Full mode also verifies the RSC antinorm certificate, with two independently written programs,
rsc/rsc-verify.pyandrsc/rsc-verify-independent.py.
cd ancillary
python3.12 -m venv .venv && .venv/bin/pip install -r requirements.txt # pinned environment
PYTHON=.venv/bin/python ./verify_all.sh # quick mode
PYTHON=.venv/bin/python ./verify_all.sh --full # full moderequirements.txt pins the tested versions (Python 3.12, python-flint 0.9.0, NumPy 2.5.4, SciPy 1.18.1). PROCS sets the number of processes of the two RSC verifiers (default 4) and LOGDIR the folder for the logs (default verify-logs/).
| Check | Mode | Time | Processes | Peak memory | Expected output |
|---|---|---|---|---|---|
| checksums and 13 checkers | quick | about 1 minute | 1 | 87 MiB | ok, same as <name>.out for each, then All checks passed. |
rsc/rsc-verify.py |
full only | about 46 minutes | 4 | about 1.4 GiB, all processes | VERIFIED |
rsc/rsc-verify-independent.py |
full only | about 16 minutes | 4 | about 3.0 GiB, all processes | VERIFIED |
Times: the quick mode on an Apple M3 Max (2026-10-30); the two RSC verifiers in the author’s recorded runs (rsc/rsc-verify.out, rsc/rsc-verify-independent.out). Peak memory of the two RSC verifiers: summed over all processes, sampled every 0.5 s in a full run with four processes at research commit 404e863, whose certificates and checkers are those of this release (Python 3.12.10, 2026-10-31), which took 75 and 24 minutes on that machine. Appendix F of the paper says what each checker certifies, and the formalisation page lists the files of each certified statement.
Checking the Lean proofs
The Lean project uses Lean v4.35.0 and Mathlib v4.35.0, pinned in lean/lean-toolchain and lean/lake-manifest.json.
cd lean
lake exe cache get
lake build
lake env lean CheckDecls.leanCheckDecls.lean checks that every declaration linked from the paper in the project’s default target exists and prints its axioms. The axiom audit in axioms.txt is the output of that command in the author’s fresh build of this release (Lean 4.35.0, Katana, 2026-11-01, of the research repository at commit 708d928, whose Lean files are those of this release; the site’s copy differs only in comments; the same file is evidence/axioms.txt). Each of these declarations uses only Lean’s standard axioms propext, Classical.choice and Quot.sound (two of them only propext and Quot.sound), and none depends on sorryAx. The formalisation page says what each Lean theorem covers.
The Lean check of the RSC antinorm certificate data is a separate target: its data files are generated from ancillary/rsc/rsc-certificate.json.gz, and its generated theorems are decided by native_decide, so they trust the Lean compiler as well as the kernel (in the author’s release build on 8 cores, both targets together took 117 minutes; ancillary/README.md gives the commands). lean/CheckDeclsData.lean checks the declarations of this target that the paper links. Its axiom audit from the author’s build of this release is evidence/axioms-data.txt: besides the standard axioms, these declarations depend on the auxiliary axioms that native_decide adds for the generated theorems only. The full mode of verify_all.sh checks the same certificate with two independent programs.
What each build of this site checks
On every change, the site’s build renders the pages and checks their links, and runs the quick mode of verify_all.sh. It does not build the Lean project: the Lean check of this release is the author’s fresh build above, and the build copies its axiom audit to axioms.txt. It runs the full mode only when started by hand with full set, so a passing build of the site means that the quick checks passed. The full verification of the RSC certificate is a separate claim, with its own log.