The listed facts are provable in ZF. Do you know of any natural ZF theorems of analysis that need countable choice when working in these sorts of subsystems? Btw since I’m not the only commenter on your answer you need to @ me for me to be notified if you respond.

I see. Sifting through your papers, I think the arguments justifying my previous comment are formalizable in $Z_2^{\Omega},$ and that this theory is a conservative extension of $Z_2$ which has third-order objects in its ontology. Is my understanding correct?

@JamesHanson Even full HB does not imply there is an np ultrafilter on $\mathbb{N},$ see jstor.org/stable/2272118 Thm 2. Incidentally, full UFL can be decomposed into the ordering principle (OP) and compactness for ordered languages (CfO), the latter implying "HB-for-sep-normed-spaces." I've been investigating the conjecture that OP and CfO are separately (but not together) consistent with a total, isometry-invariant extension of Lebesgue measure on $\mathbb{R}^n.$

The chain in your PS isn't quite right. HB does not imply ADC. In fact, UFL holds and countable choice fails in the Cohen model with an infinite Dedekind finite set of reals.

I'm confused about your (A) vs (B) dichotomy. Bounded variation functions and semi-continuous functions are in Baire class 1, and Baire class 2 is the same as effective Baire class 2. These are all provable in much less than ZF (say, $Z_2$).

@JamesHanson Sorry my previous comment was just following up on whether Riemannian manifolds are second countable. I haven’t checked if the Prufer manifold can be paracompact.

For a connected Riemannian manifold, I think this works: fix $p,$ an $(n-1)$-sphere $S$ centered at $p,$ and a countable dense $X \subset S.$ For points $q$ of rational distance from $p$ via a geodesic through a point in $X,$ take the balls $B(q, 1/n).$

@JamesHanson A second countable manifold is a Polish space, so Shoenfield applies and you get basically the whole ZFC theory, include embeddings into $\mathbb{R}^n.$ I don’t know if being connected metrizable or even a connected Riemannian manifold is enough to prove second countability.

@JamesHanson They’re inequivalent. It’s a ZF theorem that the long line is not metrizable (if an ordinal $\alpha$ has a metric, one can can transfinitely construct a canonical enumeration for each $\beta \le \alpha$).

@JamesHanson But without choice, it’s consistent that the long line is paracompact (this is equivalent to $\omega_1$ being singular). I bet it’s consistent with ZF that all manifolds are paracompact.

@IlyaBogdanov Sorry to repeatedly ping you, but I've now proven the claim for Noetherian rings.

I added a counterexample for a general commutative ring.

I've generalized the claim to Dedekind domains. I don't think this argument can be pushed much further, but it's plausible the claim holds for arbitrary Noetherian domains.