Certificates, programs and Lean formalization for "A lower bound of 0.8366 for Lebesgue's universal covering problem"

Certificates, programs and Lean proofs for the paper A lower bound of 0.8366 for Lebesgue's universal covering problem (doi:10.5281/zenodo.23717911). The paper proves that every convex set in the plane that contains a congruent copy of every set of diameter at most 1 has area at least 0.8366; the previous lower bound was 0.83474, due to J. Hatchett (doi:10.5281/zenodo.22135010). Let D be the disk of diameter 1, let Bn be the regular Reuleaux n-gon of width 1, and let M(T1, …, Tm) be the least area of the convex hull of congruent copies of T1, …, Tm. In this notation, Theorem 1.1 of the paper states M(D, B3, B5, B7) ≥ 0.836 and M(D, B3, B5, B7, B9) ≥ 0.8366, and Proposition 4.2 states M(D, B3, B5) ≥ 0.8347; it is a test of the method in the five-dimensional space of placements of D, B3 and B5. Each bound rests on a certificate, stored in parts: a grid of cells on a box of placements of the bodies (the root box), with a binary tree of boxes in each cell. At each leaf the checker verifies in ball arithmetic that the hull area exceeds the bound, mostly by a second-order Taylor bound for the area of a polygon in the hull (Section 3 of the paper). A certificate is accepted when every part passes the checker with no failure and the tree decoder confirms that the leaves tile the root box; all three certificates were accepted. A second verifier, written separately from the checker, re-verified all 16,193,402 leaves of the certificate for the five bodies with a bound that does not use the Taylor expansion. The Lean proofs (Lean 4 with Mathlib) state these inequalities for M and their consequences for universal covers, also in the weakest reading of the problem (convex sets that contain a congruent copy of every convex set of diameter 1). They check certificates of their own, on root boxes of their own divided into cells. Each of the three bounds has a proof whose checks all run in the Lean kernel (for 0.8366 the theorems hull5_geK, main5K and weak_main5K); these proofs use only the axioms propext, Classical.choice and Quot.sound. The bound 0.8366 also has a proof that runs its certificate checks as compiled code with native_decide, which adds one auxiliary axiom for each of its 75,061 certificate modules. Cost. Checking the certificates took about 3 minutes for cert5d_08347, 2.7 hours for cert8d_0836 and 395 hours for cert11d_08366 (wall-clock time per process, summed over the parts, on loaded servers). The first pass of the second verifier over the leaves of cert11d_08366 took 3,959.7 CPU-hours. Building the Lean proofs in single-threaded processes takes about 200 hours for 0.8347, 1,440 hours for 0.836, 83,000 hours for the kernel-checked proof of 0.8366 and 940 hours for the proof of 0.8366 with compiled checks. Files. The files are grouped by bound. In the file names, 5d, 8d and 11d give the dimension of the space of placements; k5, k8 and k11 mark the Lean proofs whose checks run in the kernel, and l11 the Lean proof of 0.8366 with compiled checks. The zip is identical to the tag v9 of the GitHub repository github.com/tejasvi/lebesgue-cover-bound, commit 10af98606c98ca9ffd0d9f402cae1e2efe74b792. cert11d_08366.tar.xz: the certificate of M(D, B3, B5, B7, B9) ≥ 0.8366 (2,048 parts), with the checker's output from its first run on every part and copies of the checker and the search program as they were used. full11_pass1.tar.xz: the output of the first pass of the second verifier on all leaves of cert11d_08366. The later passes, which verified the leaves that the first pass left, are in the zip's independent/full11/ directory together with their programs. l11_sources.tar.zst: the 77,175 generated Lean modules of the proof of 0.8366 with compiled checks (its certificate and final theorems), with a SHA256SUMS_lean file for them. l11_oleans.tar.zst: the compiled .olean files of these modules, with a SHA256SUMS_olean file, for loading the final theorems and printing their statements and axioms without compiling the modules again. k11_sources_00.tar to k11_sources_15.tar: the generated Lean modules of the 2,048 cells of the kernel-checked proof of 0.8366, one archive P<c>.tar.gz per cell exactly as it was built (the cell's leaf modules and the modules that walk its tree), in contiguous ranges of cells. k11_glue.tar.zst: the 75,126 modules of this proof generated from the trees before the build: the modules that walk the trees of the cells (also in the cell archives), the 64 modules that collect the cells and the root module with the final theorems. k11_sums.tar.zst: the SHA-256 lists of the sixteen k11_sources files, of every generated module and of every compiled file of the build (406,921 .olean files), the range of cells in each k11_sources file, and tables of the generated modules. The compiled files themselves (about 238 GB) are not archived; with these lists a rebuild can be compared file by file. cert8d_0836.tar.xz: the certificate of M(D, B3, B5, B7) ≥ 0.836 (24 parts). k8_sources.tar.zst: the 9,034 generated Lean modules of the proof of 0.836 (its certificate for M(D, B3, B5, B7) ≥ 0.836, its tree checks and its final theorems). k8_oleans.tar.zst: the compiled .olean files of these modules. cert5d_08347.tar.xz: the certificate of M(D, B3, B5) ≥ 0.8347 (16 parts). k5_sources.tar.zst: the 821 generated Lean modules of the proof of 0.8347 (its certificate for M(D, B3, B5) ≥ 0.8347, its tree checks and its final theorems) and its search output. k5_oleans.tar.zst: the compiled .olean files of these modules. SHA256SUMS: the SHA-256 checksums of the other files. lebesgue-cover-bound-10af98606c98.zip: the two smaller certificates, the checker, the tree decoder, the second verifiers and decoders with their output on cert11d_08366, the tests of the checker, the numerical minimization, the search programs, the Lean project with the four formal proofs (formal/), CHECKS.md and the LaTeX source of the paper. Checksums. Besides SHA256SUMS, the file CHECKS.md in the zip lists the size and SHA-256 of each archive and of the tar file that it decompresses to, and the directory that each archive holds. Checking. The checker needs Python 3 (tested with 3.12), NumPy (tested with 2.5) and python-flint (tested with 0.9). To check all parts of the main certificate, unpack the zip, place cert11d_08366.tar.xz in certificates/ (the zip contains the other two archives), extract the three archives there, and run python3 -I ../checker/lbcheck.py cert11d_08366 $(seq 0 2047) in certificates/. The parts can be checked in parallel. The command python3 -I ../checker/treecheck.py cert11d_08366 checks that the leaves tile the root box. To repeat the check that every leaf was verified by the second verifier, link independent/cert11d_08366 to the extracted certificate, place full11_pass1.tar.xz in independent/full11/, extract it there, and run python3 -I pass23/final11.py in that directory; it should print "ALL 16193402 LEAVES VERIFIED". The README lists all commands and the second verifiers; formal/README.md describes how to build and check the four Lean proofs (Lean 4 v4.35.0-rc3, Mathlib at the same tag). Version 9. The text of the paper is revised; the results, the certificates and the proofs are those of version 8. The zip and SHA256SUMS are new, and the zip adds CHECKS.md, certificates/README.md, independent/README.md and the LaTeX source of the paper.