Solution (source code)

= Solution

Put $q_k(n)=\mathbb P_p((0,0)\leftrightarrow(n,0)\text{ inside }T_k)$, with $q_k(0)=1$. The connection event is increasing in the open <edges>. Apply the <Harris-FKG inequality> to connection from $(0,0)$ to $(n,0)$ and connection from $(n,0)$ to $(n+m,0)$, both constrained to the strip. Their intersection implies connection between the outer endpoints, while horizontal translation invariance makes the second event's <probability> $q_k(m)$. Hence
$$
q_k(n+m)\geq q_k(n)q_k(m).
$$
These events may depend on infinitely many strip <edges>. To justify the inequality directly, first restrict each connecting <graph path> to a finite box, apply <Harris-FKG inequality> in the finite independent <edge> family, and then let the box grow. Every connection has a finite witness <graph path>, so continuity from below gives the stated inequality.

The direct horizontal <graph path> supplies $q_k(n)\geq p^n>0$, and <probabilities> are at most one. Thus $a_k(n)=-\log q_k(n)$ is a finite nonnegative <subadditive sequence> with $a_k(n)\leq-n\log p$. The <Fekete lemma> now gives a finite <connection decay rate in a percolation strip>:
$$
\boxed{f_k(p)=\lim_{n\to\infty}\frac{a_k(n)}n=\inf_{n\geq1}\frac{a_k(n)}n,\qquad0\leq f_k(p)\leq-\log p.}
$$
Each individual ratio is at least its <infimum>, so $-\log q_k(n)\geq nf_k(p)$ and therefore
$$
\boxed{q_k(n)\leq e^{-nf_k(p)}.}
$$
At $n=0$ this reads $1\leq1$. Only nonnegative separations are intended by this notation; horizontal reflection supplies the analogous bound with $|n|$ for negative separations.