Coherent geometric Satake conjecture for canonical-basis categories

Let $G$ be a reductive group with Langlands dual $G^\vee$, let $\mathfrak{g}$ be the adjoint representation of $G$, and let $P$ and $P^\vee$ be the weight lattices of $G$ and $G^\vee$. Let $\operatorname{Rep}G^\vee$ denote the category of finite-dimensional representations of $G^\vee$, and let $\mathcal{KP}_{G,\mathfrak{g}}$ have simple objects labeled by $P\times P^\vee$. Coherent geometric Satake conjecture. There is a monoidal functor

$$\operatorname{Rep}G^\vee\longrightarrow\mathcal{KP}_{G,\mathfrak{g}}$$

which takes the irreducible $G^\vee$-representation with highest weight $\omega^\vee$ to the simple object labeled by $(0,\omega^\vee)\in P\times P^\vee$. This is described as a coherent version of geometric Satake, reflecting the relationship between $\mathcal{D}$-modules on $\operatorname{Gr}_G$ and coherent sheaves on the cotangent bundle of $\operatorname{Gr}_G$. It is presented as a consequence of the preceding conjecture and remains unproved in the source.