Under countable choice, continuous path space is Polish

Let $(f_j)$ be $d_{\mathrm{u}\mathrm{o}\mathrm{c}}$-Cauchy and fix $n\ge 1$. For every $0<\epsilon <1$, eventually $d_{\mathrm{u}\mathrm{o}\mathrm{c}}(f_j,f_k)<2^{-n}\epsilon ,$ so its $n$th summand forces ${\max }_{t\le n}\mathrm{\mid }{f}_j(t)-f_k(t)\mathrm{\mid }<\epsilon$. Thus the restrictions to $[0,n]$ are uniformly Cauchy. By [F2]--[F3] they have a unique continuous uniform limit $g_n$.

For integers $N,M\ge 1$ and a rational tuple $(r_0,\dots ,r_{NM})$, let $p_{N,M,r}$ be linear on every interval $[k\mathrm{/}M,(k+1)\mathrm{/}M]$ with node value $r_k$, and constant after time $N$. Let $\mathcal{P}$ be the family of all these paths. For fixed $N,M$, its parameter tuples form a finite power of $\mathbb{Q}$, countable by repeated applications of [F5]--[F6]. The pairs $(N,M)$ are countable, so [F6], using the assumed ${\mathrm{A}\mathrm{C}}_{\omega }$ exactly at its countable-union clause, makes $\mathcal{P}$ countable.

Fix $f$ and $\epsilon >0$. By [F1] and the geometric tail in its definition, choose $N$ with ${\sum }_{n>N}{2}^{-n}<\epsilon \mathrm{/}2$. By [F3]--[F4], $f$ is uniformly continuous on $[0,N]$; choose $\delta >0$ so $\mathrm{\mid }s-t\mathrm{\mid }<\delta$ implies $\mathrm{\mid }f(s)-f(t)\mathrm{\mid }<\epsilon \mathrm{/}4$. By [F7], choose $M$ with $1\mathrm{/}M<\delta$, and by the density in [F5] choose the finitely many rationals $r_k$ with $\mathrm{\mid }{r}_k-f(k\mathrm{/}M)\mathrm{\mid }<\epsilon \mathrm{/}4$. For the corresponding $p\in \mathcal{P}$, convex interpolation between adjacent node errors gives ${\max }_{t\le N}\mathrm{\mid }p(t)-f(t)\mathrm{\mid }<\epsilon \mathrm{/}2.$ Hence the first $N$ metric terms sum to less than $\epsilon \mathrm{/}2$ and the tail to less than $\epsilon \mathrm{/}2$, so $d_{\mathrm{u}\mathrm{o}\mathrm{c}}(p,f)<\epsilon$.

If $m<n$, uniqueness of uniform limits makes $g_n{\mathrm{\mid }}_{[0,m]}=g_m$. Hence $f(t)=g_n(t)$ for any integer $n\ge \max (1,t)$ is well defined; equivalently use the least such integer. Its restriction to each $[0,n]$ is $g_n$, so $f$ is continuous and $f_j\to f$ uniformly on every compact interval. By [F1], $d_{\mathrm{u}\mathrm{o}\mathrm{c}}(f_j,f)\to 0$. Therefore the path-space metric is complete. No choice is used here: every $g_n$ is the unique limit.

Step 1.3 makes the countable family $\mathcal{P}$ from step 1.2 dense, so the metric space is separable. Combining this with completeness from step 2.1 and the topology identity from [F1], [F8] proves that the compact-convergence path space is Polish. Countable choice was used only in step 1.2; the finitely many rational approximations in step 1.3 are obtained by finite induction.