The global arithmetic intersection formula at nontrivial level

Let $f=\otimes_p f_p$ be a completely decomposed pure tensor in the indicated partial Hecke algebra at nontrivial level, and let $f'=\otimes_v f'_v$ be a Gaussian test function on $G'=\operatorname{Res}_{F/F_0}(\mathrm{GL}_{n-1}\times\mathrm{GL}_n)$ whose finite part is a smooth transfer of $f$. Assume that $f$ has regular support at a place $\lambda$ of $F_0$.

Global arithmetic intersection conjecture at nontrivial level. One has

$$\operatorname{Int}(f)=-\partial J(f')-J(f'_{\mathrm{corr}}),$$

where $f'_{\mathrm{corr}}\in C_c^\infty(G'({\mathbb A}))$ is a correction function. Moreover, $f'$ may be chosen to have regular support at $\lambda$ and to satisfy $f'_{\mathrm{corr}}=0$.

This extends the global arithmetic intersection formula to nontrivial level structure and asserts compatibility with correction terms. The source gives no evidence that it has been proved.