Prove $\aleph_{\omega+1}\not\to(\aleph_{\omega+1},3,\ldots,3)^2_{\aleph_0}$ in ZFC without GCH (Erdős #1168)

Prove, without assuming the generalised continuum hypothesis, the negative partition relation $$\aleph_{\omega+1}\not\to(\aleph_{\omega+1},\,3,\ldots,3)^2_{\aleph_0}.$$ In words: exhibit a colouring of the pairs (2-element subsets) of a set of size $\aleph_{\omega+1}$ using $\aleph_0$ colours such that there is no colour-$0$ homogeneous set of size $\aleph_{\omega+1}$ and, for each of the remaining $\aleph_0$ colours, no monochromatic triangle — and establish this in ZFC alone.

Acceptance. FULLY RESOLVES: a complete ZFC proof (using no set-theoretic hypotheses beyond ZFC, in particular not GCH), machine-checkable in Lean/Coq preferred, of $\aleph_{\omega+1}\not\to(\aleph_{\omega+1},3,\ldots,3)^2_{\aleph_0}$ — concretely, a definable colouring of $[\aleph_{\omega+1}]^2$ into $\aleph_0$ colours together with a proof that it omits a colour-$0$ homogeneous set of size $\aleph_{\omega+1}$ and every monochromatic triangle in the other colours. ADVANCES: a proof of the relation under a hypothesis strictly weaker than GCH, with the hypothesis stated precisely and its role discussed; or a ZFC proof of a closely related weaker negative arrow on $\aleph_{\omega+1}$; in each case with full proof. Deliver the written or formalised proof together with the explicit colouring.