Certificates, programs and Lean formalization for "The Steiner ratio is at least 0.8564"

Certificate files, programs, logs, control runs and two Lean formalizations for the paper The Steiner ratio is at least 0.8564 (doi:10.5281/zenodo.23716009). The Steiner ratio of the Euclidean plane is the infimum of the length of a Steiner minimal tree divided by that of a minimum spanning tree; Gilbert and Pollak conjectured that it equals √3/2 ≈ 0.8660, and the conjecture is open. Ke, Huang, Shu, He, Gai and Wang proved with a computer-assisted method that it is at least 0.8559. The paper proves that it is at least 2141/2500 = 0.8564. It uses their splitting tables and a modified version of their generator of boxes, gives complete proofs of the geometric lemmas that its certificate uses, adds two new bounds for the terminals outside the local configuration that extend the published ones, and bounds the networks that reconnect four points by explicit networks. The computer-assisted step consists of inequalities on 555,102,905 boxes in four families of local configurations of a Steiner minimal tree, two for each of the two types of configuration in the paper, according to which of two edge lengths, f and d, is larger: each box carries a splitting of the tree whose cost bound is checked at the vertices of the box in ball arithmetic, and the boxes of each family tile its parameter space. Files. Eight certificate files, compressed with xz, two for each family: d_regular_f_ge_dv: type d_regular, f ≥ d, 10,376,823 records, Lean data data_C1.tar.xz; d_steiner_f_ge_d: type d_steiner, f ≥ d, 12,696,761 records, Lean data data_C2.tar.xz; d_regular_f_le_d: type d_regular, f ≤ d, 95,569,010 records, Lean data data_C3.tar.xz; d_steiner_f_le_d: type d_steiner, f ≤ d, 436,460,311 records, Lean data data_C4.tar.xz.The record file <family>_certificate.bin.xz has a box, a splitting and a lemma set in each record, and the tree file <family>_child.bin.xz holds the tree of boxes. Uncompressed they have 94,104,688,256 bytes; MANIFEST.txt in the zip lists the size and SHA-256 of each file before and after decompression. data_C1.tar.xz to data_C4.tar.xz: the data of the Lean proofs, each holding the tree of boxes of its family as a stream of codes. They can be regenerated from the certificate files. lean_kernel_lists.tar.xz (63,906,192 bytes): the hash lists of the kernel-checked proof, that is, the SHA-256 of the source of every generated unit module and of the three compiled files of every unit module, every aggregator module and the final module, against which a rebuild can be compared. steiner-ratio-bound-99f1d7369809.zip (identical to the tag v4 of the GitHub repository github.com/tejasvi/steiner-ratio-bound/tree/v4, commit 99f1d7369809171ee9d495ba15c58fa4e2d3cc59): the record checker and the coverage program, the splitting tables, the generator, the logs of all runs, the control runs, the programs behind Proposition 6.1 of the paper, checks of identities used in its proofs, the two Lean projects (lean/ and lean_kernel/) and the LaTeX source of the paper. SHA256SUMS: checksums of the files in this record. Checking. After xz -d, the coverage program checks that the boxes of a family tile the orthant [0, ∞)n of its coordinates, and the checker, which needs FLINT 3, checks the records; checking all records takes about 200 core-hours. All records pass, and the logs in the zip record these runs. In the control runs, listed in the README in the zip, inputs on which the programs must fail all fail: the certificate checked at slightly larger values of the bound, altered records, a removed record and small certificates that violate conditions of the bounds. Lean. Both Lean projects (Lean v4.35.0-rc3, Mathlib commit c55e6e786f49) prove that (2141/2500)·LMST(P) ≤ LSMT(P) for every finite set P of points in the plane. They assume three named hypotheses: HTrap: the paper’s bounds for the positions of the two terminals outside the local configuration (the hidden terminals), under their conditions; HDomain: the parameters of every configuration lie in the domain of its type; HDuHwang: if every configuration has an entry of the tables with cost at most 0, the ratio bound holds for every finite set (the splitting lemma of Du and Hwang, the reduction to the two configurations, the definition of the hidden terminals, the case of at most four points, the fact that the table entries are splittings, and the induction on the number of points). The paper proves these facts, except two that are checked by programs: that the table entries are splittings (checker/split43.py) and that the tables are transcribed correctly into numeric form (checker/splits2num.py). None of these facts is proved in Lean. The certificate theorem is proved in Lean without hypotheses: for every parameter in the domain, there are a table entry and a lemma set whose conditions are satisfied and whose cost bound at 2141/2500 is at most 0, where the edges at the hidden terminals are priced by the lemma bounds. The project in lean/ (S43.Final.steiner_ratio_ge, S43.Final.certificate) runs the checking program as compiled code through native_decide, so its trusted base includes the Lean compiler and runtime. The project in lean_kernel/ (S43K.Final.steiner_ratio_ge, S43K.Final.certificate, with the same statements) checks every record with decide +kernel and relies on Lean’s kernel instead of code generated by Lean’s compiler. Both proofs were also rebuilt independently on other machines; for the kernel-checked proof every compiled file matched the hash lists (CHECKS.md in the zip describes these rebuilds). Licences. The splitting tables and the generator come from the code of Ke et al. and are under the MIT License; the other programs, including the Lean files, are under the Apache License 2.0, and the certificate files, the data files, the hash lists and the logs are under CC BY 4.0. The README in the zip describes the file formats, the commands and the controls, and the READMEs of the two Lean projects describe their trusted bases, axioms and builds, and that of lean/ also its build time and hardware. Version 4 accompanies version 4 of the paper; apart from the copy of the repository, which adds the LaTeX source of the paper and a description of the independent checks of the Lean proofs and has an updated README, the files are those of version 3.