Coherent completeness and formal functions for geometrically reductive quotient stacks

Let $R$ be a complete noetherian local ring, let $G$ be a smooth geometrically reductive group scheme over $R$, and let $X=\operatorname{Spec} A$ be an affine scheme of finite type over $R$ with an action of $G$ such that $A^G=R$. Let $x\in [X/G]$ be the unique closed point, and let $\mathcal{G}_x$ be its residual gerbe. A noetherian algebraic stack is cohomologically proper over a noetherian ring if the cohomology of every coherent sheaf is a finitely generated module in every degree. A pair consisting of a noetherian algebraic stack and a closed substack is coherently complete when the natural functor from coherent sheaves on the stack to coherent sheaves on its formal completion is an equivalence, and it satisfies formal functions when the natural maps from the cohomology of coherent sheaves to the cohomology on the formal completion are isomorphisms in every degree.

Coherent completeness and formal functions conjecture. The stack $[X/G]$ is cohomologically proper over $A^G$, and the pair $([X/G],\mathcal{G}_x)$ is coherently complete and satisfies formal functions.

The statement appears under the paper's “Main conjecture and results” section and specializes the broader quotient-stack conjecture to a smooth geometrically reductive group scheme over a complete local base. The supplied text gives no evidence of resolution, so its status is open.