Supercritical continuity of percolation probability (source code)

= Supercritical continuity of percolation probability

Independent <site percolation> and <bond percolation> on the <cubic lattice> have continuous <percolation probability> on $(p_c,1]$. Fix $p>p_c$ and an intermediate $q\in(p_c,p)$. By <uniqueness of the infinite percolation cluster>, every origin in the infinite $p$-cluster has a finite $p$-open <graph path> to the infinite $q$-cluster. In the uniform-label <monotone coupling of Bernoulli percolation>, the finitely many labels on this <graph path> are strictly below fixed $p$ <almost surely>, so it persists at some parameter below $p$. The <coupled onset parameter for origin percolation> has no attained atom there, giving left continuity, including at $1$. Combine this with <right continuity of percolation probability>.