Essential enhancements of site percolation in every dimension

In 1991 Aizenman and Grimmett gave an argument that an essential enhancement of percolation strictly lowers the critical probability. Balister, Bollobás and Riordan later found that a combinatorial lemma in that argument is false. They reduced the case of site percolation on Zd to a deterministic statement about rerouting paths, proved it for d = 2 and d = 3, and left the cases d ≥ 4 open. We prove their Conjecture 1 for site percolation on Zd for every d ≥ 2. The proof does not confine the enhancement gadget to the ball centred at the pivotal site. Instead it allows any ℓ1 ball that lies in a large ball around that site, has radius bounded below by a fixed constant, and meets the pivotal path in at least three sites. A two-port theorem, valid in every dimension, shows that the gadget can be wired in unless the first and last sites of the path in the ball form a corner pair. A compactness and mass-transport argument shows that some admissible ball avoids this configuration. As in the cases d = 2, 3, the result rests on the probabilistic part of the Aizenman–Grimmett argument. The deterministic part of the argument, Claim 5 of Balister, Bollobás and Riordan, is also checked in the Lean proof assistant for every d ≥ 2. Mathematics Subject Classification (2020): Primary 60K35; Secondary 82B43.