in [@Boch Section 9], an alternative construction for the $p$-stabilisation of a Siegel modular form of integral weight which method does guarantee that $f_0\neq 0$, if $f\neq 0$.

\[pstabprop\] If $f\in\mathcal{M}_k(\Gamma[{\mathfrak}{b}^{-1}, {\mathfrak}{bc}], \psi)$ is an eigenform and $p\nmid{\mathfrak}{c}$, then $f_0\in\mathcal{M}_k(\Gamma[{\mathfrak}{b}^{-1}, {\mathfrak}{bc}_0], \psi)$ where ${\mathfrak}{c}_0 = {\mathfrak}{c}p^{2(2^n-1)}$. Moreover, $$f_0|U_p = \left(p^{\frac{n(n+1)}{2}}\lambda_{p, 1}\cdots \lambda_{p, n}\right)f_0.$$

Define $W_p := \Gamma_0\left(\begin{smallmatrix} pI_n & 0 \\ 0 & p^{-1}I_n\end{smallmatrix}\right)\Gamma_0\in\mathcal{R}_{0p}$; clearly $f|W_p = p^{nk}f(p^2z)$ has level $\Gamma[{\mathfrak}{b}^{-1}, {\mathfrak}{bc}p^2]$ and therefore, as operators, $W_p\Gamma[{\mathfrak}{b}^{-1}, {\mathfrak}{bc}p^2] = W_p$. Let $\alpha^{\iota} := \det(\alpha)\alpha^{-1}$ denote the standard involution on invertible matrices and extend this to $\mathcal{R}_{0p}$ by putting $(\Gamma_0\alpha\Gamma_0)^{\iota} = \Gamma_0\alpha^{\iota}\Gamma_0$. The elements $W_p$ and $U_p$ satisfy $U_p = W_p^{\iota}$ and, by the argument of [@Panchishkin p. 49], we have $U_p\Gamma[{\mathfrak}{b}^{-1}, {\mathfrak}{bc}p^2] = U_p$ as operators as well. So $f|U_p\in\mathcal{M}_k(\Gamma[{\mathfrak}{b}^{-1}, {\mathfrak}{bc}p^2], \psi)$ and the first property follows by definition of $f_0$ and $V_m$.

Set $\lambda_0 := p^{\frac{n(n+1)}{2}}\lambda_{p, 1}\cdots \lambda_{p, n}$. The second property is given by the calculation $$\begin{aligned}
    f_0|[\lambda_0-U_p] &= \lambda_0 f_0|[1-\lambda_0^{-1}U_p] \\
        &=\lambda_0 f\bigg|\left[\sum_{m=0}^{2^n-1}(\lambda_0^{-1})^mV_{m, p}\right][1-\lambda_0^{-1}U_p] \\
    &=\lambda_0f|R_n(\lambda_0^{-1}),\end{aligned}$$ where Proposition \[Rfact\] was invoked in the last line and Definition \[pstab\] in the penultimate. This is zero since we have $f|R_n(\lambda_0^{-1}) = \widetilde{R}_n(\lambda_{p, 1}, \dots, \lambda_{p, n}; \lambda_0^{-1})f$ and $(1-\lambda_0z)$ 