Which limit ordinals $\alpha$ force every graph on $\alpha$ to have an infinite path or an independent set of type $\alpha$? (Erdős #601)

Let $\alpha$ be a limit ordinal and let $G$ be a graph whose vertex set is $\alpha$ (a graph on a well-ordered vertex set of order type $\alpha$). Say $\alpha$ has the property if EVERY such graph $G$ must contain at least one of: an infinite path, or an independent set (a set of pairwise non-adjacent vertices) whose vertices form a subset of order type $\alpha$. For which limit ordinals $\alpha$ does this property hold?

Acceptance. FULLY RESOLVES: a complete proof characterizing exactly the limit ordinals $\alpha$ with the property — in ZFC where the answer is absolute, and with the set-theoretic hypotheses clearly flagged wherever the answer is independent of ZFC — or, at minimum, a complete proof settling the general case that Erdős priced at \$500. Deliver a full written proof with all steps (machine-checkable Lean/Coq preferred). ADVANCES, each with a complete proof: resolve the specific boundary ordinal $\alpha=\omega_1^{\omega+2}$ (the \$250 sub-question); extend the Erdős–Hajnal–Milner range beyond $\omega_1^{\omega+2}$ to a new class of ordinals in ZFC; or establish new consistency or independence results (e.g. remove the Martin's-Axiom hypothesis from Larson's theorem for a stated subclass, or prove a failure is consistent). Deliver the proof.