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

Part 3 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.chosen.part4.xz: piece 4 of 4 of the file of entries k30e.chosen, compressed (bytes 447,973,982,208 to 597,298,560,191 of the uncompressed file); 15,710,030,624 bytes, SHA-256 769cbb866ccf71bb87bf21e05c01bd7657916fae64b799c928ef21638d579e48. k30e.v.part1.xz: piece 1 of 5 of the file of weights k30e.v, compressed (bytes 0 to 39,819,935,743 of the uncompressed file); 29,573,851,700 bytes, SHA-256 64b54eeffa168503b464d39c0174b78b5d91c2e1f45cee45ec0b1594c136dcc6. SHA256SUMS: the SHA-256 checksums of the files of this record.