Does $\omega_1^2\to(\omega_1\omega,G)^2$ hold for every $K_4$-free, $K_{\aleph_0,\aleph_0}$-free graph $G$? (Erdős #597)

The ordinal partition arrow $\beta\to(\alpha,G)^2$ means: for every $2$-colouring of the edges (unordered pairs) of the complete graph on a vertex set well-ordered with order type $\beta$, either there is a subset of vertices of order type $\alpha$ all of whose pairs receive the first colour (a first-colour homogeneous set of type $\alpha$), or there is a copy of the graph $G$ all of whose edges receive the second colour. Let $G$ be a graph on at most $\aleph_1$ vertices that contains no $K_4$ and no $K_{\aleph_0,\aleph_0}$ (the complete bipartite graph with $\aleph_0$ vertices in each class). Is it true that $$\omega_1^2\to(\omega_1\omega,\,G)^2\,?$$ In particular, does the relation hold for every finite such $G$?

Acceptance. FULLY RESOLVES: a complete proof that $\omega_1^2\to(\omega_1\omega,G)^2$ holds for every $K_4$-free, $K_{\aleph_0,\aleph_0}$-free graph $G$ on at most $\aleph_1$ vertices; OR a counterexample — a specific such $G$ together with a proof that the relation fails (a $2$-colouring witnessing failure). Deliver a full written proof with all steps, or a machine-checkable proof (Lean/Coq preferred). ADVANCES, each with a complete proof: settle the finite-$G$ case; prove the relation for a natural subclass (e.g. all $K_4$-free graphs of bounded degree, or all finite bipartite $G$); or strictly generalize the Erdős–Hajnal $K_3$ result toward the full statement. Deliver the proof.