Choice in the non-smooth Whitney Embedding Theorem Introduction
In Munkres' Topology, he presents a precursor of what seems to be called the non-smooth Whitney Embedding Theorem in Section 50:

Theorem 50.5 (The imbedding theorem). Every compact metrizable space $X$ of [Lebesgue covering] dimension $m$ can be embedded in $\Bbb{R}^{2m+1}$.

(By the way, let me know if this has its own name.) He goes on to use this to prove every compact $m$-manifold can be embedded in $\Bbb{R}^{2m+1}$.
Looking over his proof, it appears that the full Axiom of Choice is not required. The only possibly problematic statements are the following:

*

*There exists a partition of unity $(\phi_i)$ subordinate to a finite open covering $\{U_1, \cdots, U_n\}$ of $X$.

*The space $\mathcal{C}(X, \Bbb{R}^{2m+1})$  is a Baire space under the uniform topology.

However, the first statement is choice-free because $X$ is a metric space and so Urysohn's lemma holds on $X$; one can use Munkres' proof in Section 36 from there. But the second statement a priori requires Dependent Choice ($\mathsf{DC}$).
$\mathsf{DC}$ can be avoided if we could prove that $\mathcal{C}(X, \Bbb{R}^{2m+1})$ was in fact separable. This brings me to my question.

The Question
Can we prove that $X$ being compact metric implies that $\mathcal{C}(X, \Bbb{R})$ is separable in the uniform topology in $\mathsf{ZF}$ alone? If not, what if $X$ is itself separable? ("Compact metric implies separable" requires Countable Choice.) What if $X$ is a topological manifold? (Here a manifold is assumed to be second-countable Hausdorff.) If still the answer is no, must we use $\mathsf{DC}$ in the cited theorem as discussed, or can we get away with weaker choice principles?

Some Known Things

*

*This answer proves that for any compact Hausdorff $X$, $\mathcal{C}(X, \Bbb{R})$ is separable iff $X$ is metrizable (in $\mathsf{ZFC}$ at worst). We would only need the $(\impliedby)$ direction here, but the answer uses the Stone-Weierstrass theorem, and I'm not convinced S-W can be gotten choice-free. I am happy to be wrong on that front though, if in fact we can get S-W.


*I know that it holds in $\mathsf{ZF}$ that every manifold is metrizable, and also compact manifolds are separable (they are a finite union of chart domains, which are necessarily separable).


*It may not be useful, but since I really just want to know the answer of the question for compact manifolds, we could assume $X$ is path-connected (i.e., look at components of the compact manifold).
 A: Stone-Weierstrass does not require Choice.  For example, the proof in Lang's Real and Functional Analysis (p. 52-54) uses Choice to pick functions $h_{x,y}$ that separate each pair of points, but you can avoid that by just using all such functions for each $x$ and $y$ rather than one particular fixed function.  Then it uses a choice of finite subcover to define a function $h_x$ for each point $x$, but again you can instead just consider all functions which have the required properties of $h_x$ instead of choosing one in particular.
So, ZF can prove that $C(X,\mathbb{R})$ is separable if $X$ is a separable compact metric space.  On the other hand, if $X$ is a compact metric space such that $C(X,\mathbb{R})$ is separable, then a countable dense subset of its unit ball gives an embedding $X\to [-1,1]^\mathbb{N}$.  Any closed subspace $X\subseteq [-1,1]^{\mathbb{N}}$ is separable: pick a countable dense subset $\{a_n\}$ of $[-1,1]^{\mathbb{N}}$, and then it suffices to pick an element of $X$ which is in each closed ball of rational radius around an $a_n$ that intersects $X$.  This can be done without Choice by just taking the least element of the intersection with respect to the lexicographic order (which exists by compactness).  Thus ZF cannot prove that $C(X,\mathbb{R})$ is separable for every compact metric space $X$, since then it would be able to prove that every such $X$ is separable.
