[proofplan] Assume the uniform compactness principle $\mathsf{CTBSC}$. The standard constructive interval $[0,1]$ is displayed as a complete totally bounded [metric space](/page/Metric%20Space) by its usual Cauchy-real completion and rational grids, so the principle gives [sequential compactness](/page/Sequential%20Compactness) of $[0,1]$. Given a decidable infinite binary tree, choose one node on each level and encode it as a point of the Cantor ternary set. A convergent subsequence of these ternary codes has tails of arbitrarily small diameter, and the ternary separation estimate forces all sufficiently late tree nodes to share each fixed finite prefix. These compatible prefixes form an infinite path through the tree, proving Weak König's Lemma. [/proofplan]

[step:Apply the assumed compactness principle to the represented interval]Assume $\mathsf{CTBSC}$. Let $I := [0,1]$ be the standard represented constructive interval, and let $\mathbb{R}_{\geq 0} := \{r \in \mathbb{R} : r \geq 0\}$. Equip $I$ with the usual metric $d_I: I \times I \to \mathbb{R}_{\geq 0}$ given by $d_I(x,y) = |x-y|$. The usual construction of located Cauchy [real numbers](/page/Real%20Numbers) supplies a Cauchy-completion operation for Cauchy sequences in $I$ equipped with moduli; the order bounds $0 \leq x_n \leq 1$ pass to the constructed limit, so the limit again lies in $I$. For each $m \in \mathbb{N}$, define the rational grid \begin{align*} G_m := \left\{ \frac{q}{2^m} : q \in \{0,1,\dots,2^m\} \right\} \subseteq I. \end{align*} This is a finite subset of $I$. Since the represented interval is located, for every $x \in I$ the rational approximation procedure at precision $2^{-(m+1)}$ produces a rational $r \in [0,1] \cap \mathbb{Q}$ with $|x-r| \leq 2^{-(m+1)}$. Choose $q \in \{0,1,\dots,2^m\}$ with $|r-q2^{-m}| \leq 2^{-(m+1)}$, which is possible by finite search over the displayed grid. The triangle inequality gives \begin{align*} \left|x-\frac{q}{2^m}\right| \leq |x-r| + \left|r-\frac{q}{2^m}\right|. \end{align*} Since both terms on the right are at most $2^{-(m+1)}$, we obtain \begin{align*} \left|x-\frac{q}{2^m}\right| \leq 2^{-m}. \end{align*} Thus $G_m$ is a finite $2^{-m}$-net. Therefore $I$ is a displayed complete and totally bounded metric space in the sense required by $\mathsf{CTBSC}$. Applying $\mathsf{CTBSC}$ to $I$, every sequence in $I$ has a displayed convergent subsequence: a strictly increasing subsequence map, a [limit point](/page/Limit%20Point) in $I$, and a convergence modulus.[/step]

[guided]We first isolate exactly where the assumed principle is used. The principle $\mathsf{CTBSC}$ applies only to metric spaces whose compactness data are displayed: we need a metric, a completion operation for Cauchy sequences with moduli, and finite nets at each precision. For the interval $I := [0,1]$, define $\mathbb{R}_{\geq 0} := \{r \in \mathbb{R} : r \geq 0\}$. The metric is the map \begin{align*} d_I: I \times I \to \mathbb{R}_{\geq 0}, \qquad d_I(x,y) = |x-y|. \end{align*} The usual constructive construction of located Cauchy real numbers gives the required completion operation: a [Cauchy sequence](/page/Cauchy%20Sequence) in $I$ together with a modulus determines its limit as a constructive real, and the bounds $0 \leq x_n \leq 1$ pass to that limit, so the limit belongs to $I$. [Total boundedness](/page/Total%20Boundedness) is also displayed explicitly. For each $m \in \mathbb{N}$, define \begin{align*} G_m := \left\{ \frac{q}{2^m} : q \in \{0,1,\dots,2^m\} \right\}. \end{align*} This is finite because $\{0,1,\dots,2^m\}$ is finite. Given $x \in [0,1]$, use the located representation of $x$ to compute a rational approximation $r \in [0,1] \cap \mathbb{Q}$ satisfying $|x-r| \leq 2^{-(m+1)}$. Since the displayed grid is finite, finite search over $q \in \{0,1,\dots,2^m\}$ finds a grid point with $|r-q2^{-m}| \leq 2^{-(m+1)}$. The triangle inequality then gives \begin{align*} \left|x-\frac{q}{2^m}\right| \leq |x-r| + \left|r-\frac{q}{2^m}\right|. \end{align*} Since each term on the right is at most $2^{-(m+1)}$, we conclude \begin{align*} \left|x-\frac{q}{2^m}\right| \leq 2^{-m}. \end{align*} Hence $G_m$ is a finite $2^{-m}$-net for I. So all hypotheses of $\mathsf{CTBSC}$ are satisfied by the standard represented interval. The conclusion is that every sequence in $[0,1]$ has a convergent subsequence together with a displayed convergence modulus. This modulus is the compactness input used later to choose, for each precision, a stage after which all subsequence terms are close.[/guided]

[step:Choose level witnesses in the decidable infinite binary tree] Let $T \subseteq 2^{<\mathbb{N}}$ be a decidable binary tree with a node at every finite level. Here $2^{<\mathbb{N}}$ denotes the set of finite binary strings, and $2^n$ denotes the finite set of binary strings of length $n$. Thus, for every $n \in \mathbb{N}$, there exists a string in $T \cap 2^n$. Because $T$ is decidable and $2^n$ is finite, finite search produces a distinguished witness \begin{align*} w(n) \in T \cap 2^n \end{align*} for each $n \in \mathbb{N}$, for instance the lexicographically least element of $T \cap 2^n$. Write \begin{align*} w(n) = (w(n)_1,\dots,w(n)_n) \end{align*} with each digit $w(n)_i \in \{0,1\}$. [/step]

[step:Encode the level witnesses as ternary Cantor points] Define a sequence \begin{align*} x: \mathbb{N} \to I \end{align*} by \begin{align*} x_n := \sum_{i=1}^{n} \frac{2w(n)_i}{3^i}. \end{align*} Since each $w(n)_i$ is either $0$ or $1$, each summand is non-negative and \begin{align*} 0 \leq x_n \leq \sum_{i=1}^{n} \frac{2}{3^i} \leq \sum_{i=1}^{\infty} \frac{2}{3^i} = 1. \end{align*} Thus $x_n \in I$ for every $n \in \mathbb{N}$. By the displayed sequential compactness of $I$, there exist a strictly increasing map $k: \mathbb{N} \to \mathbb{N}$, a point $x_\infty \in I$, and a convergence modulus $M: \mathbb{N} \to \mathbb{N}$ such that, for every $r \in \mathbb{N}$ and every $\ell \geq M(r)$, \begin{align*} |x_{k_\ell}-x_\infty| < 2^{-r}. \end{align*} [/step]

[step:Prove that incompatible binary prefixes have separated ternary codes]For a finite binary string $s = (s_1,\dots,s_n) \in 2^n$, define its ternary code by $c(s) := \sum_{i=1}^{n} \frac{2s_i}{3^i}$. Fix $j \in \mathbb{N}$ with $j \geq 1$. Suppose $s \in 2^p$ and $t \in 2^q$ for some $p,q \in \mathbb{N}$ with $p \geq j$ and $q \geq j$, and suppose the first $j$ digits of $s$ and $t$ are not equal. Let $r \in \{1,\dots,j\}$ be the least index such that $s_r \neq t_r$. Then \begin{align*} |c(s)-c(t)| \geq 3^{-r} \geq 3^{-j}. \end{align*} Indeed, the first unequal digit contributes exactly $2\cdot 3^{-r}$ to the absolute difference, while all later digits together can cancel by at most \begin{align*} \sum_{i=r+1}^{\infty} \frac{2}{3^i} = 3^{-r}. \end{align*} Therefore the remaining uncancelled difference is at least $3^{-r}$.[/step]

[guided]The purpose of the ternary encoding is that binary disagreement becomes metric separation. Let \begin{align*} c: 2^{<\mathbb{N}} \to [0,1] \end{align*} be the map defined on a finite binary string $s = (s_1,\dots,s_n)$ by \begin{align*} c(s) := \sum_{i=1}^{n} \frac{2s_i}{3^i}. \end{align*} Only the ternary digits $0$ and $2$ occur. This gap between allowed digits is what prevents two different prefixes from being arbitrarily close. Fix a prefix length $j \in \mathbb{N}$ with $j \geq 1$. Let $s \in 2^p$ and $t \in 2^q$ with $p,q \in \mathbb{N}$, $p \geq j$, and $q \geq j$, and suppose $s$ and $t$ do not have the same first $j$ digits. Let $r \in \{1,\dots,j\}$ be the least index such that $s_r \neq t_r$. At digit $r$, the two ternary codes differ by exactly $2 \cdot 3^{-r}$. Digits after $r$ can partially cancel this difference, but their total possible contribution is bounded by \begin{align*} \sum_{i=r+1}^{\infty} \frac{2}{3^i}. \end{align*} Evaluating the geometric series gives \begin{align*} \sum_{i=r+1}^{\infty} \frac{2}{3^i} = 3^{-r}. \end{align*} Hence the absolute difference between the two codes satisfies \begin{align*} |c(s)-c(t)| \geq 2\cdot 3^{-r} - 3^{-r} = 3^{-r}. \end{align*} Since $r \leq j$, we also have $3^{-r} \geq 3^{-j}$. Therefore \begin{align*} |c(s)-c(t)| \geq 3^{-j}. \end{align*} This is the key quantitative fact: if two encoded tree nodes are closer than $3^{-j}$, then their first $j$ binary digits must agree.[/guided]

[step:Extract a common prefix at each finite length]Fix $j \in \mathbb{N}$ with $j \geq 1$. Choose $r_j \in \mathbb{N}$ such that $2^{1-r_j} < 3^{-j}$. Let $L_j := M(r_j)$. If $a,b \geq L_j$, then the triangle inequality and the defining property of the convergence modulus give \begin{align*} |x_{k_a}-x_{k_b}| \leq |x_{k_a}-x_\infty| + |x_{k_b}-x_\infty| < 2^{1-r_j} < 3^{-j}. \end{align*} Choose $a \geq L_j$ with $k_a \geq j$, which is possible because $k$ is strictly increasing. Define $s_j \in 2^j$ to be the length-$j$ prefix of $w(k_a)$. If $b \geq L_j$ and $k_b \geq j$, then the separation estimate from the previous step shows that the length-$j$ prefixes of $w(k_a)$ and $w(k_b)$ are equal; otherwise the corresponding ternary codes would be at distance at least $3^{-j}$, contradicting \begin{align*} |x_{k_a}-x_{k_b}| < 3^{-j}. \end{align*} Thus $s_j$ is independent of the chosen sufficiently late index $a$. Since $w(k_a) \in T$ and $T$ is a tree, every initial segment of $w(k_a)$ belongs to $T$. Hence \begin{align*} s_j \in T \cap 2^j. \end{align*}[/step]

[guided]The compactness principle supplied more than a bare existential convergent subsequence: it supplied the convergence modulus $M: \mathbb{N} \to \mathbb{N}$. We use that modulus to produce the stage at which all relevant encoded nodes have a common prefix. Fix $j \in \mathbb{N}$ with $j \geq 1$. Choose $r_j \in \mathbb{N}$ such that $2^{1-r_j} < 3^{-j}$. This choice is effective because powers of $2$ eventually dominate any fixed positive rational bound. Define $L_j := M(r_j)$. If $a,b \geq L_j$, then the modulus gives \begin{align*} |x_{k_a}-x_\infty| < 2^{-r_j} \end{align*} and \begin{align*} |x_{k_b}-x_\infty| < 2^{-r_j}. \end{align*} The triangle inequality in the metric interval $I$ therefore yields \begin{align*} |x_{k_a}-x_{k_b}| \leq |x_{k_a}-x_\infty| + |x_{k_b}-x_\infty| < 2^{1-r_j} < 3^{-j}. \end{align*} Now choose $a \geq L_j$ with $k_a \geq j$; such an $a$ exists because $k: \mathbb{N} \to \mathbb{N}$ is strictly increasing and hence unbounded. Define $s_j \in 2^j$ to be the length-$j$ prefix of the tree node $w(k_a)$. To see that this definition does not depend on the particular sufficiently late $a$, take any $b \geq L_j$ with $k_b \geq j$. If the length-$j$ prefixes of $w(k_a)$ and $w(k_b)$ differed, the ternary separation estimate would give \begin{align*} |x_{k_a}-x_{k_b}| \geq 3^{-j}, \end{align*} contradicting the bound just proved. Hence all sufficiently late nodes in the subsequence have the same length-$j$ prefix. Finally, since $w(k_a) \in T$ and $T$ is a tree, every initial segment of $w(k_a)$ lies in $T$. The string $s_j$ is exactly such an initial segment, so \begin{align*} s_j \in T \cap 2^j. \end{align*}[/guided]

[step:Assemble the compatible prefixes into an infinite path] We now show that the sequence of finite strings $(s_j)_{j \in \mathbb{N}}$ is compatible, using the convention $\mathbb{N}=\{1,2,3,\dots\}$ and digit positions indexed from $1$. Let $i,j \in \mathbb{N}$ with $i \leq j$. Choose $a$ sufficiently large so that $a \geq L_i$, $a \geq L_j$, and $k_a \geq j$. By the construction of $s_i$ and $s_j$, the string $s_i$ is the length-$i$ prefix of $w(k_a)$, and $s_j$ is the length-$j$ prefix of $w(k_a)$. Therefore $s_i$ is the length-$i$ prefix of $s_j$. Define $\alpha: \mathbb{N} \to \{0,1\}$ by declaring $\alpha_i$ to be the $i$-th digit of $s_j$ for any $j \geq i$. Compatibility shows that this definition is independent of the chosen $j$. For every $j \in \mathbb{N}$, the length-$j$ prefix of $\alpha$ is exactly $s_j$, and we proved $s_j \in T$. Thus every nonempty finite prefix of $\alpha$ lies in $T$, so $\alpha$ is an infinite path through $T$. Since $T$ was an arbitrary decidable binary tree with a node at every finite level, $\mathsf{CTBSC}$ implies Weak König's Lemma. This proves that the constructive principle “complete and totally bounded implies sequentially compact” is not constructively valid as a uniform principle unless Weak König's Lemma is available. [/step]