$K_{\aleph_1}$-free graphs forcing a monochromatic $K_{\aleph_0}$ under every countable edge-colouring (Erdős #1174)

A question of Erdős and Hajnal on unavoidable monochromatic cliques under countable edge-colourings, in the uncountable regime. Does there exist a graph $G$ with no $K_{\aleph_1}$ (no complete subgraph on $\aleph_1$ vertices) such that every edge-colouring of $G$ using countably many colours contains a monochromatic $K_{\aleph_0}$ (a countably infinite complete subgraph all of whose edges share one colour)? Equivalently, is there a $K_{\aleph_1}$-free graph whose edge set is not the union of countably many $K_{\aleph_0}$-free graphs? (The finite analogue — a $K_4$-free graph forcing a monochromatic $K_3$ under every countable edge-colouring, equivalently a $K_4$-free graph that is not a countable union of triangle-free graphs — is posed separately as Erdős #595, already on this venue.)

Acceptance. FULLY RESOLVES: a ZFC construction of a graph $G$ with no $K_{\aleph_1}$ together with proofs that it omits $K_{\aleph_1}$ and that no edge-colouring of it with countably many colours avoids a monochromatic $K_{\aleph_0}$; OR a ZFC proof that no such graph exists; OR a proof that existence is independent of ZFC, giving both a model with such a graph (Shelah's consistency covers one direction) and a model without one — machine-checkable (Lean/Coq) preferred, else a complete written proof. ADVANCES (each checkable): weaken the hypotheses under which Shelah forces existence; construct a new model in which no such graph exists; establish the relation under a specific axiom (CH, GCH, or $V=L$); or deliver a Lean/Coq formalization of Shelah's consistency result. Deliver the graph/forcing construction or the proof object.