This should also give the more general fact that $\aleph^*(X^{<\omega}) \le \aleph^*(X)^+.$

I'd call this fact "near-productivity of Lindenbaum numbers," while non-productivity refers to ZF models in which this inequality is sharp (see here for an example mathoverflow.net/a/456549/109573).

I appreciate you calling it "my argument" but I definitely don't have the model theory chops to have ironed out the details here in any reasonable amount of time. Thank you so much for completing this! I came up with the idea trying to answer this mathoverflow.net/questions/127041/…. I might as well go answer that now that we have a precise result.

It does not. Even the Hahn-Banach theorem does not imply that $\omega$ (or any set) admits a non-principal ultrafilter. See Pincus and Solovay's Definability of Measures and Ultrafilters. I wouldn't be surprised if their model of HB with no np ultrafilters in fact has that all diffuse measures have range $[0,1].$

Is it even clear that Hahn-Banach implies there is a diffuse measure whose range is not $[0,1]$?

Yes, $n_{\alpha}$ is what I meant. And the redundant "standard" was just there as signposting, but I removed it since it might have just been confusing.

@JoelDavidHamkins Agreed, my original assertion was imprecise. For any complete $T$ with an infinite model, any $p = (p', T),$ TFAE: (1) $V=\mathrm{HOD}_p,$ (2) the schema "any two $\Sigma_n(q)$-definable PCS models of $T$ with satisfaction predicate admit a $\Sigma_{n+2}(p,q)$-definable isomorphism," (3) two particular PCS models having some $OD_p$ bijection.

I also believe the latter argument shows global choice to be equivalent to the surreals being in bijection with the Kanovei-Shelah hyperreal class, since Ord canonically embeds into No.

I think for any complete theory $T$ with an infinite model, global choice is equivalent to any two proper class saturated (PCS) models of $T$ being isomorphic (or even just having a definable bijection). It would be enough to define PCS models $M_0, M_1 \models T$ where $\mathrm{Ord} \subset M_0$ and for all $\alpha,$ for all but set-many $x \in M_1,$ $x$ constructs a well-ordering of $\mathcal{P}(\alpha).$ I believe the Kanovei-Shelah construction gets a model with the latter property, and we can get $M_0$ by adjusting that construction to include an Ord-sequence of indiscernibles.

Reference for the above claim^ irif.fr/~krivine/articles/Modeles_de_ZF_CRAS.pdf

In $L^{\mathrm{Col}(\omega, \omega_1)}$ all OD sets of reals are measurable, so I don't think there's going to be any reasonable answer to this question.