@GuozhenShen: An old theorem of Truss says that if there is some $\alpha$ such that there are no chains of type $\alpha$ (of distinct cardinals) between $X$ and $\mathcal P(X)$, then the axiom of choice holds.

I think that pretty much anything (reasonable) can be made compatible with $V=\rm HOD$ and $\sf GCH$.

Now that the question had been changed entirely, it's an interesting question. I'd suggest to change the name from $\sf GCH^{WO}$ to something else. This is no longer a generalised continuum hypothesis in any sense of the word. Perhaps "Linear Interval Power Set", or $\sf LIPS$.

@AndrésE.Caicedo is correct. The atoms have no bearing on Specker's proof. If you suspect that it doesn't, simply go through it and edit your question to point out where exactly the assumption that we work in $\sf ZF$ comes into the proof.

Oh, that's an interesting question. I don't know.

Sure. Look at the set of injective finite sequences, then look at the map which trims the last element from the sequence. It's in a few answers around the site, I'm certain, and you can play with the proof even more to get other crazy ideas.

Supercompactness without choice cannot, and should not, be defined via ultrafilters. If Łoś theorem fails, which it bounds to with AC failing this hard, then ultrafilters, and certainly ultrafilters over ordinals, are practically meaningless. What you want to talk about is embeddings.

Oh, I see what you're asking for now. Sure, that can also work. But I was aiming for correct, not optimal.

If we started with $A$ strictly larger, how would that come to be?

It's not well founded... I don't understand your question.

@YnirPaz: The point is that $\alpha\mapsto A_\alpha$ is an amenable class function, and we can add a predicate for $\{A_\alpha\mid\alpha\in\rm Ord\}$. And moreover, the union of these sets is itself Dedekind-finite.

Ducking auto portrait.

Apologies for the bad citation formatting, I'm typing this on my phone.

To add to what @Wojowu said, this happens in the Cohen model.