# Code of the computer-assisted proofs

Code and data of the computer-assisted steps of *Path Decompositions of Sparse Graphs via
Gaussian Sweeps and Faster Exponential Algorithms* (Serge Gaspers), under the MIT licence
(`LICENSE`). `SHA256SUMS` lists the checksum of every file. The files keep the paths they
have in the research repository, so the scripts run unchanged from this folder; comments
that pointed to unpublished working notes now name the corresponding statement of the paper
or were removed. Statement numbers in comments that do not say "of the paper" are those of the
research notes or of earlier drafts.

## Contents

| Folder | What it computes | Paper |
|:--|:--|:--|
| `experiments/arb-certificates/` | the certificate of the admissible pair and triples (Arb ball arithmetic and exact rational recheck), the enclosure of F_4, and the charging certificate of the median-switched sweep | Proposition 7.5, Proposition 6.9, Proposition A.13 |
| `experiments/reproducibility/` | the driver `run_all.sh`, the Arb bounds for F_3 (`F/`), the exact arithmetic of the main theorem, the stored logs (`outputs/`) and pinned versions (`requirements.txt`) | Appendix A.2.6 |
| `experiments/degree-bootstrap-check.py` | randomized tests of the bootstrap inequality | Lemma 9.3 |
| `experiments/switch-lemma-degree3/`, `experiments/switch-lemma-degree4/` | the box certificates of the switch lemma with unequal bounds (box lists for d = 3; per-part summaries for d = 4, whose full box lists of about 11 GB the search programs regenerate) | Lemma A.10 |
| `experiments/pathwidth-sequences/` | the bootstrap table in exact rational arithmetic | Corollary 9.5 |
| `experiments/algorithmic-consequences/` | the constants and branching analyses of Part II and Appendices C and D | Part II, Appendix C, Appendix D |
| `experiments/sweep-algorithms/` | the implementation of the randomized algorithms and its tests | Appendix B.1 |

## Running the main certificate

With Python 3.14 and the versions in `experiments/reproducibility/requirements.txt`
(`python-flint`, NumPy, SciPy, mpmath), from this folder:

```sh
PY=python3 sh experiments/reproducibility/run_all.sh quick   # about one minute
PY=python3 sh experiments/reproducibility/run_all.sh full    # about 80 minutes on 16 cores
```

The quick mode rechecks the stored cells in exact arithmetic; the full mode recomputes the
Arb enclosures and the certificate, rewrites the stored cell files and rechecks them (compare
the cell files with `SHA256SUMS`). Both modes write their logs to
`experiments/reproducibility/outputs/`. The logs stored there are those of the full-mode runs of
2026-10-07 and 2026-10-10 (the Arb bounds of F_3 and F_4, the certificate and its rerun) and of the
bootstrap tests; the output of the S-switched problem, added later, is
`experiments/arb-certificates/star-bound-arb-owen-S-switched-output.txt`. Logs of the quick-mode
checks are not stored, because those checks changed after the stored runs; the quick mode writes
them. The research driver also checked a result that is not part of this paper; that line was
removed.

The `lean` mode expects the Lean project in `lean/` next to `experiments/`; on the site the Lean
project is the folder `lean/` at the top level, and the formalisation page says how it was built.
That mode also prints the SHA-256 of two specification files, to compare with the approved digests
in `run_all.sh`. The site's copies have comments with references to unpublished notes removed, so
their digests differ from the approved ones, which are those of the research repository at commit
`e1fa7cf`:

| File | Approved (research repository) | Site copy |
|:--|:--|:--|
| `lean/CubicPathwidth/C3Spec.lean` | `5ffd69d0d86747f9dcad8b566de485425cdb3d6d5d47775f316b4431dcaff644` | `2c33b1d1f62431cbf6f2592fb827997c3347811936073e82cc0e8084151f591e` |
| `lean/CubicPathwidth.lean` | `dce37d2a898241cf34f03dffc25bdcb0d675fd7edaabf5017f3b119ef2f9ccdf` | `80f18b540959d2ad57336eb369abe9783815021c928f503683cf319c862ba6aa` |