Modularity conjecture for elliptic curves over quadratic imaginary fields

Let $K$ be a quadratic imaginary field of class number one, let $p>3$ be a prime, and let $E$ be an elliptic curve over $K$. Write $G_K$ for the absolute Galois group of $K$, and let $\overline{\rho}_E:G_K\to\operatorname{GL}_2(\overline{\mathbb F}_p)$ be the mod $p$ representation on the $p$-torsion of $E$. Suppose that $\overline{\rho}_E$ is absolutely irreducible and continuous, has Serre conductor $\mathcal N$, and that its restriction to $G_{K_{\mathfrak p}}$ arises from a finite-flat group scheme over $\mathcal O_{K_{\mathfrak p}}$ for every prime $\mathfrak p\mid p$. Modularity conjecture over $K$. There is a mod $p$ eigenform $c\in H^1(Y_0(\mathcal N),\overline{\mathbb F}_p)$ such that, for every prime ideal $(\pi)\subseteq\mathcal O_K$ coprime to $p\mathcal N$,

$$T_\pi(c)=\operatorname{Trace}\bigl(\overline{\rho}_E(\operatorname{Frob}_{(\pi)})\bigr)\cdot c.$$

This is the number-field analogue of Serre's modularity statement; the supplied text does not establish its resolution.