Solution (source code)

= Solution

Let $c_n$ count $n$-step <self-avoiding walks> on the <square lattice> from one fixed <graph vertex>. Splitting a <self-avoiding walk> after $m$ steps and dropping the avoidance constraint on its suffix gives $c_{m+n}\leq c_mc_n$. The <Fekete lemma> therefore gives the <connective constant> $\mu=\lim c_n^{1/n}$. The <planar dual graph> of the <square lattice> is a translated copy of it, so its <connective constant> is also $\mu$.

Put $q=1-p$ and assume $q\mu<1$. Choose $a>\mu$ with $qa<1$. The definition of the <connective constant> provides a finite $K$ such that $c_j\leq Ka^j$ for every $j\geq0$. A simple dual <graph cycle> of length $\ell$ surrounding $0$ has a <graph vertex> in a box of radius $\ell+1$: its diameter is at most $\ell$, and its coordinate ranges straddle the origin. Choose such a <graph vertex> as the starting point, orient the <graph cycle>, and omit its closing <edge>. The remaining <self-avoiding walk> has length $\ell-1$. Consequently the number $N_\ell$ of these <graph cycles> obeys
$$
N_\ell\leq K_0\ell^2 c_{\ell-1}\leq K_1\ell^2a^{\ell-1}
$$
for fixed finite constants. A specified <graph cycle> is open in <dual bond percolation>, equivalently all its crossed primal <edges> are closed, with <probability> $q^\ell$. Hence
$$
\sum_{\ell\geq L}N_\ell q^\ell\longrightarrow0\quad\text{as }L\to\infty.
$$
To make this tail argument valid for every $q\mu<1$, rather than only extremely small $q$, use a <finite modification of Bernoulli percolation>. Condition all primal <edges> within $\Lambda_N$ to be open. This event has positive <probability> for $p>0$. If the resulting <percolation cluster> of $0$ is finite, its outer boundary contains a simple closed dual <graph cycle> surrounding the whole box. Such a <graph cycle> has length tending to infinity with $N$ and crosses no forced-open <edge>. Under the conditioning its remaining <edge> states retain the original independent law, so its <probability> is still $q^\ell$. Choose $N$ so that the above tail is less than $1/2$. The conditional <probability> that $0$ belongs to an <infinite percolation cluster> is then at least $1/2$, and thus $\theta(p)>0$.

This <connective-constant Peierls bound> proves that every $p>1-\mu^{-1}$ is above or at the onset of positive <percolation probability>. Taking the infimum gives
$$
\boxed{p_c\leq1-\mu^{-1}}.
$$
The case $p=1$ is immediate. This proof uses the <Peierls argument>, without assuming the exact <Harris-Kesten theorem>.