Data and programs for "Certified lower bounds on the optimal-decoding threshold of the surface code"

This record holds the data behind the paper "Certified lower bounds on the optimal-decoding threshold of the surface code". It contains the registration of the Monte Carlo certificate of Theorem 2.5 with its timestamp proofs, the registered programs, the 600,000 sample records of the run and the output of the final analysis. It also contains the certificate of Theorem 2.6 under measurement errors, with its validations repeated at the registered window radius, and the counting certificates of Theorems 2.1 to 2.4 together with their generators and checkers. The outputs of all checks are included too, as are the paper's two supplements: the records supplement, which collects the records of the experiments and of the formal checks, and the criterion supplement, which holds the single-scale criterion with its proof. The file SHA256SUMS lists the SHA-256 of the two supplements (PDF and source of each), the five archives, their checksum lists and normalized_files.tsv; the paper gives the SHA-256 of SHA256SUMS. Each archive unpacks with zstd -dc NAME.tar.zst | tar -x, and its checksum list gives the SHA-256 of every unpacked file; counting.SHA256SUMS covers both counting archives. README.md explains how to check the hashes and timestamps, repeat the acceptance check of the certificate, and run the row checks of the counting certificates. The Lean proofs of the theorems are in a separate record (10.5281/zenodo.23778262).