# Ancillary files of "Monotone Local Search with Sample-Dependent Running Times"

These files are the computer-checked parts of the proofs in the paper. The section "Computer certificates"
of the paper describes each check in detail; this file is the short manifest.

## Running the checks

```
python3.12 -m venv .venv && .venv/bin/pip install -r requirements.txt   # pinned environment
PYTHON=.venv/bin/python ./verify_all.sh          # quick: every check a proof depends on, except the two RSC certificate verifiers
PYTHON=.venv/bin/python ./verify_all.sh --full   # full: also the two RSC certificate verifiers
```

Requirements: Python 3 with python-flint, NumPy and SciPy; `requirements.txt` pins the versions we tested
(Python 3.12.16, python-flint 0.9.0, NumPy 2.5.4, SciPy 1.18.1). The same commands work in a container,
for example `docker run --rm -v "$PWD":/anc:ro python:3.12-slim bash -c 'cp -r /anc /tmp/a && cd /tmp/a &&
python -m venv /tmp/v && /tmp/v/bin/pip install -r requirements.txt && PYTHON=/tmp/v/bin/python ./verify_all.sh'`.
The script first checks the SHA-256 checksums in `SHA256SUMS`, then runs each program and compares its output
with the recorded output of the author's run (the `.out` file of the same name, ignoring timing lines; for
the two RSC verifiers it requires the line `VERIFIED`). It stops at the first program that fails or whose
output differs. Options are set through environment variables: `PYTHON` (interpreter), `PROCS` (processes
for the RSC verifiers, default 4) and `LOGDIR` (where the output of each program is written, default
`verify-logs/`); relative paths are taken from the current folder. The script uses only POSIX shell tools
and runs with the BSD tools of macOS as well as with GNU coreutils.

The quick and the full mode certify different things. "All checks passed" after the quick mode means that
every check of the table below passed except the RSC antinorm certificate (Prop. `prop:rsc-cert`); only
the full mode verifies that certificate, with two independent programs.

| Mode | What it runs | Time | Processes | Peak memory |
| --- | --- | --- | --- | --- |
| quick | checksums and the 13 programs above the RSC verifiers | about 62 s (Apple M3 Max, 2026-10-30, and the same result in `python:3.12-slim` under Docker) | 1 | 87 MiB |
| full, extra | `rsc/rsc-verify.py` | about 46 minutes in the recorded run (first lines of `rsc/rsc-verify.out`) | 4 (`PROCS`) | about 1.4 GiB, all processes (2026-10-31) |
| full, extra | `rsc/rsc-verify-independent.py` | about 16 minutes in the recorded run (timestamps in `rsc/rsc-verify-independent.out`) | 4 (`PROCS`) | about 3.0 GiB, all processes (2026-10-31) |

## The RSC certificate

`rsc/rsc-certificate.json.gz` (45 MB) is not in the arXiv copy of these files, because arXiv stores gzip files
unpacked (156 MB, over its size limit). It is in the archived copy of this release (Zenodo,
https://doi.org/10.5281/zenodo.23851002) and on the companion site (https://serggasp.github.io/sample-MLS-site/);
put it into `rsc/`. Its SHA-256 checksum is in `SHA256SUMS`. Without it, `verify_all.sh` runs every check except
the two RSC verifiers of `--full`.

## Which file checks which statement

| Statement in the paper | Files | Arithmetic |
| --- | --- | --- |
| Constant 1.744835 of RS and the two bounds on F* used by RS-θ (Prop. `prop:rs-rate`(c)) | `rs_closed_form_interval.py` | exact rationals; Arb ball arithmetic |
| The two antinorm certificates of RS-θ and the bounds on c_Z (Prop. `prop:rst-certs`) | `cert_final_0.json`, `cert_final_1.json`, `verify_cert.py`, `verify_cert_indep.py`, `v_cert_primal.py`, `cz_bounds.py` | exact rationals |
| Rates of the RS-θ certificates and 2^ψ* < 1.7204 (Props. `prop:rst-certs`, `prop:rst-rate`) | `rst_rate_interval.py` | exact rationals; Arb |
| Bounds 1.71927 and 1.71928 for the uniform lobsters (Prop. `prop:rst-caterpillar`(c)) | `lobster_rate_certificate.py` | exact rationals |
| Antinorm certificate of RSC (Prop. `prop:rsc-cert`), two independent programs | `rsc/rsc-certificate.json.gz`, `rsc/rsc-verify.py` (with `rsc/rsc_verify_core.py`, `rsc/rsc_modelg.py`), `rsc/rsc-verify-independent.py` | exact rationals |
| Credit inequalities and light pairs of RSC (Lemmas `lem:rsc-rsccredits`, `lem:rsc-lightpairs`) | `rsc/rsc-credits.py` | exact rationals |
| Endpoint inequalities of the deterministic rate certificate (Lemma `lem:det-cert`) | `rates.py` (part 4), `v_rates.py` (part V1) | exact rationals |
| Constant 1.6444 for Graph Motif and Connected Vertex Cover (Lemma `lem:cc-cert`) | `component_count_rate_interval.py` | exact rationals; Arb |
| Three certificates and constant 1.3727 for Directed Steiner Tree (Prop. `prop:fa-dst-certs`) | `dst_certificates.json`, `dst_certificate_verify.py`, `cz_bounds.py` | exact rationals; Arb |
| Constant 1.6302 for Paired Domination (Lemma `lem:fa-pd-rate`) | `paired_rate_certificate.py` | Arb |

The other programs (second table of the section "Computer certificates") compute numerical evidence that no
proof uses. The folder `formal/` contains the Lean 4 development described in the subsection "Formal
verification"; build it with `lake build` (the files `lean-toolchain` and `lake-manifest.json` pin the
versions of Lean and Mathlib).

The Lean check of the RSC certificate data is a separate target, and it uses `native_decide`, so it trusts
the Lean compiler as well as the kernel. From this folder, regenerate the data files (about 170 MB, about 2 min)
and check them against the shipped checksums. The exporter writes its own `MANIFEST.sha256` into the output
folder, so first save the shipped one:

    cp formal/MaxLeafFormal/RSCData/MANIFEST.sha256 MANIFEST-lean-check.sha256
    python3 formal/scripts/export_rsc_cert.py rsc/rsc-certificate.json.gz formal/MaxLeafFormal/RSCData
    python3 formal/scripts/rsc_data_audit.py --scan
    python3 formal/scripts/rsc_data_audit.py --compare rsc/rsc-certificate.json.gz

The last command checks the generated data against the certificate, value by value. The shipped
`formal/MaxLeafFormal/RSCData/MANIFEST.sha256` lists the checksums of the files as they were generated for the
Lean check. Each generated file names the SHA-256 of the exporter in its header comment. The exporter shipped
here differs from the one used for the Lean check in three comment lines only, so files regenerated here differ
from those files in that one header line. Putting back the exporter's SHA-256 from the Lean check in that line
gives the checked files byte for byte, and the checksums then all match:

    cd formal/MaxLeafFormal/RSCData
    perl -pi -e 's/^(exporter sha256: +)[0-9a-f]{64}$/${1}9191995423a44b6d882afb9076aff1fa9775ae272a2ad4f1985c144344c8386b/' *.lean
    sha256sum -c ../../../MANIFEST-lean-check.sha256
    mv ../../../MANIFEST-lean-check.sha256 MANIFEST.sha256
    cd ../../..

(On macOS, `shasum -a 256 -c` replaces `sha256sum -c`.) Then run `lake build MaxLeafFormal.RSCFinal MaxLeafFormal.RSCHeadline` in
`formal/`. The author's fresh build of the whole project, the default target and the RSC data targets, against a prebuilt Mathlib, took
81 and 117 minutes in two builds on machines with 8 cores and 124 GB of memory (2026-10-31 and 2026-11-01). Each Lean process needs
up to 6 GB of memory, and the module `RSCData.Lattice` needs 14 GB, so a machine with less memory per core needs
fewer parallel jobs.

The exact value of c_Z and the stages of the RSC certificate are the further target
`lake build MaxLeafFormal.RSCFinalExtras`. Its six further generated theorems (also decided by `native_decide`)
and their assembly are shipped in `formal/MaxLeafFormal/RSCData/Extras/`, with their checksums. The scripts
`formal/scripts/export_rsc_extras.py` and `formal/scripts/rsc_extras_audit.py`, which wrote and audited these
files, first check the SHA-256 of the exporter and of `rsc_data_audit.py` as they were used for the Lean check,
so they stop at that check here, because the copies shipped here differ from those in comments. They are not
needed to rebuild: their outputs are shipped.

The ancillary files are released under the MIT licence; see `LICENSE`.