The site percolation threshold of the square lattice is at most 0.632, and one random completion per cell creates a giant cluster

We give a computer-assisted argument that Bernoulli site percolation on the square lattice ℤ2 has an infinite cluster at density 79/125 = 0.632, so that pcsite(ℤ2) ≤ 0.632; the best published rigorous upper bound is 0.666894. The argument is a two-stage site substitution: site percolation on the line graph of ℤ2, whose threshold is 1/2 by Kesten's theorem, is compared first with an intermediate lattice and then with ℤ2, using vertex-disjoint 6 × 6 blocks in the first stage and the same blocks shifted by (3, 3) in the second. Each stage reduces to a stochastic domination inequality between two explicit laws on the boundary connectivity states of one block. Both inequalities are certified by exact integer max-flow certificates, and an independent program, which computes the block laws and all masses itself, has checked both certificates. Since 0.632 < 1 − 1/e, the bound settles a question on random completion of a grid. We prove that if cn2 cells of an n × n grid are completed, each chosen uniformly at random with repetition, then the largest cluster of completed cells has (θ(1 − e−c) + o(1)) n2 cells with high probability when 1 − e−c > pcsite(ℤ2), where θ is the percolation probability, and O(log n) cells when 1 − e−c < pcsite(ℤ2). With the new bound the first case includes c = 1, one completion per cell on average. MSC 2020: 60K35 (primary); 82B43, 05C80, 68V05 (secondary) Files: the paper (PDF), its LaTeX source (ZIP), the programs that enumerate the block laws and produce and check the certificates, including an independent checker (ZIP), and the certificate data (a compressed archive in parts).