Certificate of order 30, part 1 of 5, for "An upper bound for the connective constant of the square lattice"

Part 1 of 5 of the certificate of order 30 for the paper An upper bound for the connective constant of the square lattice (doi:10.5281/zenodo.23574053). The paper proves that the connective constant μ of self-avoiding walks on the square lattice satisfies μ ≤ 105432502045487/39656386815908 = 2.658651241600… < 2.6586513. The certificate consists of three files, 995.5 GB in all: the keys of its 24,887,440,008 states, the entries (the table of children) and the weights. They were compressed with xz: the file of keys as a whole, the file of entries in four pieces and the file of weights in five. The ten compressed files, which take 210.4 GB, are spread over five records: doi:10.5281/zenodo.23574056, doi:10.5281/zenodo.23574058, doi:10.5281/zenodo.23574060, doi:10.5281/zenodo.23574062 and doi:10.5281/zenodo.23574064. The programs, the README and the Lean formalization are in the record doi:10.5281/zenodo.23574054; the README in its zip file describes the format of the files, how to join the pieces and how to check the certificate. Files. k30e.keys.xz: the whole file of keys k30e.keys, compressed; 17,690,904,620 bytes, SHA-256 2666650fe83c65c2a4653973f256dc8ff640b51617c15b8781e6077def486d8d. k30e.chosen.part1.xz: piece 1 of 4 of the file of entries k30e.chosen, compressed (bytes 0 to 149,324,660,735 of the uncompressed file); 20,226,533,140 bytes, SHA-256 7b58ac22e168136d91017822c60972b38ee12d56ed003b9ca4871e2e632cf353. SHA256SUMS: the SHA-256 checksums of the files of this record.