[proofplan] The proof uses Brouwer's fan theorem in its uniform-bar form: a decidable bar on Cantor space has a uniform bound on the lengths needed to meet the bar. Applying this to the determining bar $B_f$ gives an integer $N$ such that every binary sequence has some prefix of length at most $N$ lying in $B_f$. If two elements of Cantor space agree on their first $N$ entries, then any determining prefix of one of length at most $N$ is also a prefix of the other. The definition of $B_f$ then forces the two values of $f$ to be equal. [/proofplan] [step:Apply the fan theorem to bound the determining prefixes uniformly] We use Brouwer's fan theorem in the following form: every decidable bar on $2^{\mathbb N}$ is uniform, meaning that there exists a bound on the lengths of prefixes needed to meet the bar. By hypothesis, $B_f \subseteq 2^{<\mathbb N}$ is a decidable bar. Therefore, by Brouwer's fan theorem (citing a result not yet in the wiki: Brouwer's Fan Theorem), there exists $N \in \mathbb N$ such that for every $\gamma \in 2^{\mathbb N}$ there exists $m \in \mathbb N$ with $m \leq N$ and $\gamma|m \in B_f$. [guided] The role of the fan theorem is exactly to convert a pointwise bar condition into a uniform one. The bar condition says that for each individual path $\gamma \in 2^{\mathbb N}$, some finite prefix of $\gamma$ lies in $B_f$. This prefix may initially depend on $\gamma$. The decidability hypothesis on $B_f$ is the additional constructive condition required by Brouwer's fan theorem. Applying Brouwer's fan theorem to the decidable bar $B_f \subseteq 2^{<\mathbb N}$ gives a single integer $N \in \mathbb N$ such that every path meets $B_f$ by length $N$. Concretely, for every $\gamma \in 2^{\mathbb N}$ there exists $m \in \mathbb N$ satisfying $m \leq N$ and $\gamma|m \in B_f$. This is the only place where the fan theorem is used. The pointwise continuity of $f$ is not needed after $B_f$ has been assumed to be a decidable bar; it is part of the usual context explaining why such determining prefixes are expected to exist. [/guided] [/step] [step:Show that agreement on the first $N$ entries preserves a determining prefix] Let $\alpha,\beta \in 2^{\mathbb N}$ satisfy $\alpha|N = \beta|N$. By the bounded-bar conclusion applied to $\gamma := \alpha$, choose $m \in \mathbb N$ such that $m \leq N$ and $\alpha|m \in B_f$. Define $s := \alpha|m \in 2^{<\mathbb N}$. Since $m \leq N$ and $\alpha|N = \beta|N$, the length-$m$ initial segments agree, so $\beta|m = \alpha|m = s$. Hence both $\alpha$ and $\beta$ extend $s$. [/step] [step:Use the defining property of $B_f$ to obtain a uniform modulus] Since $s \in B_f$, the definition of $B_f$ says that for all $\delta,\varepsilon \in 2^{\mathbb N}$ extending $s$, one has $f(\delta) = f(\varepsilon)$. Applying this with $\delta := \alpha$ and $\varepsilon := \beta$ gives $f(\alpha) = f(\beta)$. We have proved that for all $\alpha,\beta \in 2^{\mathbb N}$, the implication $\alpha|N = \beta|N \implies f(\alpha) = f(\beta)$ holds. Therefore $N$ is a [uniform continuity](/page/Uniform%20Continuity) modulus for $f$ on Cantor space, and $f$ is uniformly continuous. [/step]