Does $\omega_1^2\to(\omega_1\omega,3,\ldots,3)^2_{k+1}$ hold for every finite $k$? (Erdős #1171)

For ordinals the partition arrow $\kappa\to(\beta_0,\beta_1,\ldots,\beta_r)^2$ asserts that whenever the $2$-element subsets (pairs) of a set of order type $\kappa$ are coloured with $r+1$ colours $0,1,\ldots,r$, there is an index $i$ and a subset of order type $\beta_i$ all of whose pairs receive colour $i$. Here $\omega_1$ is the first uncountable ordinal and $\omega_1^2=\omega_1\cdot\omega_1$, $\omega_1\omega=\omega_1\cdot\omega$ are ordinal products. Is it true that for every finite $k<\omega$ $$\omega_1^2\to(\omega_1\omega,\underbrace{3,\ldots,3}_{k})^2_{k+1}?$$ That is, does every colouring of the pairs of an $\omega_1^2$-ordered set with $k+1$ colours yield either a subset of order type $\omega_1\omega$ monochromatic in colour $0$, or, for some $i\in\{1,\ldots,k\}$, a $3$-element set (a 'triangle') monochromatic in colour $i$?

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, otherwise fully written) that $\omega_1^2\to(\omega_1\omega,3,\ldots,3)^2_{k+1}$ holds for every finite $k$ (in ZFC, or under a clearly stated additional axiom together with a consistency argument), OR a proof/construction of a $k$ and a colouring of the pairs of an $\omega_1^2$-set into $k+1$ colours with no colour-$0$ set of type $\omega_1\omega$ and no monochromatic triangle in colours $1,\ldots,k$, refuting the relation. ADVANCES (each fully proved): remove or weaken Baumgartner's Martin's-axiom hypothesis for the base relation $\omega_1\omega\to(\omega_1\omega,3)^2$; establish the $(k+1)$-colour relation for a specific $k\ge 2$; or reduce the problem to the two-colour case via a stepping-up or product argument. Deliver the written or formalised proof, or the explicit colouring witnessing failure with a verification that it has no homogeneous set of the required type.