For which set-theoretic hypotheses does $2^{\aleph_0}\not\to[\aleph_1]^2_3$ hold? (Erdős #474, $100)

Under what set-theoretic assumptions can the pairs of points of the plane be $3$-coloured so as to be 'everywhere rainbow' on uncountable sets? Precisely: regarding $\mathbb{R}^2$ as a set of cardinality $2^{\aleph_0}$, for which models of set theory is there a colouring of the unordered pairs $[\mathbb{R}^2]^2$ with $3$ colours such that, for every uncountable $A\subseteq\mathbb{R}^2$, the pairs $[A]^2$ realise all three colours (each colour occurs on some pair within $A$)? In partition-calculus notation, for which hypotheses does the square-bracket relation $$2^{\aleph_0}\not\to[\aleph_1]^2_3$$ hold — i.e. there is a $3$-colouring of $[\,2^{\aleph_0}\,]^2$ such that every subset of size $\aleph_1$ has all $3$ colours on its pairs?

Acceptance. FULLY RESOLVES: settle Erdős's \$100 question — determine the set-theoretic hypotheses under which $2^{\aleph_0}\not\to[\aleph_1]^2_3$ holds. Concretely, a machine-checkable (Lean/Coq) or complete written proof that either (a) decides the relation outright in ZFC, or (b) gives a full independence characterization across values of the continuum, or (c) answers the specific open target: is $2^{\aleph_0}\not\to[\aleph_1]^2_3$ consistent with $\mathfrak{c}=\aleph_2$? — by constructing a forcing model witnessing it or proving no such model exists. ADVANCES (each checkable): a forcing model that decides the relation for a value of the continuum not previously settled (Erdős handled $\mathfrak{c}=\aleph_1$ via CH; Shelah gave a positive model at very large $\mathfrak{c}$) — in particular any rigorous progress on the $\mathfrak{c}=\aleph_2$ case; OR a consistency result strengthening or weakening Shelah's hypotheses for the positive relation; OR a Lean/Coq formalization of Erdős's CH proof or the Sierpiński–Kurepa two-colour theorem. Deliver the forcing/model construction or the proof object.