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

Part 5 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.v.part3.xz: piece 3 of 5 of the file of weights k30e.v, compressed (bytes 79,639,871,488 to 119,459,807,231 of the uncompressed file); 23,256,219,024 bytes, SHA-256 acff736d6e436931831b3da78f3d6e4061d1d5f45bf21080d85473c7903fda11. k30e.v.part4.xz: piece 4 of 5 of the file of weights k30e.v, compressed (bytes 119,459,807,232 to 159,279,742,975 of the uncompressed file); 18,408,974,248 bytes, SHA-256 e66a05539c19ab6584231d8085c0177323677d7c5017ef35f64d53b615efac24. SHA256SUMS: the SHA-256 checksums of the files of this record.