[proofplan] We encode each displayed node of the binary tree as a point of the Cantor ternary set by replacing binary digit $0$ by ternary digit $0$ and binary digit $1$ by ternary digit $2$. [Sequential compactness](/page/Sequential%20Compactness) gives a convergent subsequence of these real codes. The separation estimate for ternary codes shows that, for each fixed length $j$, the first $j$ binary digits of the subsequence are eventually constant. These eventual prefixes form a compatible family of nodes of $T$, and their union is the required infinite path. [/proofplan] [step:Encode the displayed level witnesses by ternary Cantor codes] For each $m\in\mathbb{N}$, let $2^m$ denote the set of binary strings $s=(s_1,\dots,s_m)$ of length $m$, with $s_i\in\{0,1\}$. Define the coding map $c_m:2^m\to[0,1]$ by \begin{align*}c_m(s)=\sum_{i=1}^{m}\frac{2s_i}{3^i}.\end{align*} This value lies in $[0,1]$, since $0\le c_m(s)\le \sum_{i=1}^{m}\frac{2}{3^i}<\sum_{i=1}^{\infty}\frac{2}{3^i}=1$. Define the sequence $x:\mathbb{N}\to[0,1]$ by \begin{align*}x_n=c_n(w(n)).\end{align*} By the assumed sequential compactness of $[0,1]$, there exist a strictly increasing map $\alpha:\mathbb{N}\to\mathbb{N}$ and a point $x_\infty\in[0,1]$ such that $x_{\alpha(k)}\to x_\infty$ as $k\to\infty$. [/step] [step:Prove that different length-$j$ prefixes have separated ternary codes] Fix $j\in\mathbb{N}$. If $a=(a_1,\dots,a_m)\in 2^m$ and $b=(b_1,\dots,b_n)\in 2^n$ have $m,n\ge j$ and differ among their first $j$ digits, then \begin{align*}|c_m(a)-c_n(b)|\ge 3^{-j}.\end{align*} Indeed, let $r\in\{1,\dots,j\}$ be the first index such that $a_r\ne b_r$. The contribution of the $r$-th digit to $c_m(a)-c_n(b)$ has absolute value $2\cdot 3^{-r}$. The total possible contribution of all later digits has absolute value at most \begin{align*}\sum_{i=r+1}^{\infty}\frac{2}{3^i}=3^{-r}.\end{align*} Therefore the earlier nonzero contribution cannot be cancelled completely, and \begin{align*}|c_m(a)-c_n(b)|\ge 2\cdot 3^{-r}-3^{-r}=3^{-r}\ge 3^{-j}.\end{align*} [guided] Fix a length $j\in\mathbb{N}$. The point of using ternary digits $0$ and $2$ is that two different binary prefixes cannot produce ternary codes that are arbitrarily close. Let $a=(a_1,\dots,a_m)\in 2^m$ and $b=(b_1,\dots,b_n)\in 2^n$, where $m,n\ge j$, and suppose their first $j$ digits are not equal. Let $r\in\{1,\dots,j\}$ be the first place where the two strings differ. Thus $a_i=b_i$ for every $1\le i<r$, while $a_r\ne b_r$. At the $r$-th ternary digit, the two codes differ by exactly $2\cdot 3^{-r}$ in absolute value. Later digits can partially cancel this difference, so we estimate the largest possible cancellation from all indices $i>r$. Since each later ternary digit is either $0$ or $2$, the total later contribution has absolute value at most \begin{align*}\sum_{i=r+1}^{\infty}\frac{2}{3^i}=3^{-r}.\end{align*} Thus the first differing digit leaves at least \begin{align*}2\cdot 3^{-r}-3^{-r}=3^{-r}\end{align*} of separation. Since $r\le j$, we have $3^{-r}\ge 3^{-j}$, and hence \begin{align*}|c_m(a)-c_n(b)|\ge 3^{-j}.\end{align*} This is the quantitative separation property that will convert convergence of [real numbers](/page/Real%20Numbers) into eventual agreement of binary prefixes. [/guided] [/step] [step:Extract an eventual common prefix at each finite length] Fix $j\in\mathbb{N}$. Since $x_{\alpha(k)}\to x_\infty$, there exists $K_0\in\mathbb{N}$ such that, for all $k\ge K_0$, \begin{align*}|x_{\alpha(k)}-x_\infty|<\frac{1}{2\cdot 3^{j}}.\end{align*} Because $\alpha:\mathbb{N}\to\mathbb{N}$ is strictly increasing, $\alpha(k)\ge k$ for every $k\in\mathbb{N}$. Choose $K\in\mathbb{N}$ with $K\ge K_0$ and $K\ge j$. Then, for all $k,\ell\ge K$, the witnesses $w(\alpha(k))$ and $w(\alpha(\ell))$ have lengths $\alpha(k)\ge j$ and $\alpha(\ell)\ge j$, and the triangle inequality gives \begin{align*}|x_{\alpha(k)}-x_{\alpha(\ell)}|\le |x_{\alpha(k)}-x_\infty|+|x_{\alpha(\ell)}-x_\infty|<3^{-j}.\end{align*} If the first $j$ digits of $w(\alpha(k))$ and $w(\alpha(\ell))$ differed for some $k,\ell\ge K$, then the separation estimate from the previous step would give \begin{align*} |x_{\alpha(k)}-x_{\alpha(\ell)}|\ge 3^{-j}, \end{align*} contradicting the strict upper bound just obtained. Hence the first $j$ digits of $w(\alpha(k))$ and $w(\alpha(\ell))$ agree for all $k,\ell\ge K$. Define $s_j\in 2^j$ to be this common length-$j$ prefix. Since $s_j$ is an initial segment of $w(\alpha(K))$ and $w(\alpha(K))\in T$, the tree property implies $s_j\in T$. [guided] Fix $j\in\mathbb{N}$. Convergence of the real sequence along the subsequence means that the tail of $(x_{\alpha(k)})_{k\in\mathbb{N}}$ is eventually contained in any prescribed neighbourhood of $x_\infty$. We use the neighbourhood of radius $1/(2\cdot 3^j)$: there is $K_0\in\mathbb{N}$ such that, for every $k\ge K_0$, $|x_{\alpha(k)}-x_\infty|<\frac{1}{2\cdot 3^{j}}$. Because $\alpha:\mathbb{N}\to\mathbb{N}$ is strictly increasing and $\mathbb{N}=\{1,2,3,\dots\}$, induction gives $\alpha(k)\ge k$ for every $k\in\mathbb{N}$. Choose $K\in\mathbb{N}$ with $K\ge K_0$ and $K\ge j$. Then for every $k\ge K$, the string $w(\alpha(k))$ has length $\alpha(k)\ge j$, so its first $j$ digits are defined. Now take $k,\ell\ge K$. Applying the triangle inequality in $\mathbb{R}$ to the points $x_{\alpha(k)}$, $x_\infty$, and $x_{\alpha(\ell)}$ gives $|x_{\alpha(k)}-x_{\alpha(\ell)}|\le |x_{\alpha(k)}-x_\infty|+|x_{\alpha(\ell)}-x_\infty|<3^{-j}$. The separation estimate says that two strings of length at least $j$ whose first $j$ binary digits differ have ternary codes separated by at least $3^{-j}$. We apply its contrapositive to $w(\alpha(k))$ and $w(\alpha(\ell))$: if their first $j$ digits differed, then \begin{align*} |x_{\alpha(k)}-x_{\alpha(\ell)}|\ge 3^{-j}, \end{align*} which contradicts the strict inequality above. Therefore all strings $w(\alpha(k))$ with $k\ge K$ have the same length-$j$ prefix. Call this prefix $s_j\in 2^j$. Since $s_j$ is an initial segment of $w(\alpha(K))$ and $w(\alpha(K))\in T$, closure of $T$ under initial segments gives $s_j\in T$. [/guided] [/step] [step:Verify compatibility of the finite prefixes] Let $j\in\mathbb{N}$. We prove that $s_{j+1}$ extends $s_j$. Choose $K_j\in\mathbb{N}$ such that all $w(\alpha(k))$ with $k\ge K_j$ have length at least $j$ and common length-$j$ prefix $s_j$. Choose $K_{j+1}\in\mathbb{N}$ such that all $w(\alpha(k))$ with $k\ge K_{j+1}$ have length at least $j+1$ and common length-$(j+1)$ prefix $s_{j+1}$. For any $k\ge \max\{K_j,K_{j+1}\}$, the length-$j$ prefix of $w(\alpha(k))$ is $s_j$, while the length-$(j+1)$ prefix of $w(\alpha(k))$ is $s_{j+1}$. Therefore the length-$j$ initial segment of $s_{j+1}$ is exactly $s_j$. [/step] [step:Assemble the compatible prefixes into an infinite path] Define $p:\mathbb{N}\to\{0,1\}$ as follows. Since $\mathbb{N}=\{1,2,3,\dots\}$, for each $j\in\mathbb{N}$ let $p_j$ be the $j$-th digit of $s_j$. This is well-defined because $s_j$ has length $j$. Compatibility shows that if $m\ge j$, then the $j$-th digit of $s_m$ is also $p_j$. For each $j\in\mathbb{N}$, the length-$j$ initial segment of $p$ is exactly $s_j$. Since the previous step proved $s_j\in T$, every finite initial segment of $p$ lies in $T$. Hence $p$ is an infinite path through $T$, which is the asserted recursive form of Weak König's Lemma. [/step]