Constructible bijectivity conjecture for filtered Weyl and Poisson automorphism schemes

For each $n,N\geq 1$, let ${\underline{\operatorname{Aut}}}^{\leq N}(A_{n,\mathbb Q})$ and ${\underline{\operatorname{Aut}}}^{\leq N}(P_{n,\mathbb Q})$ denote the filtered automorphism schemes, and let

$$\phi_{n,N}:{\underline{\operatorname{Aut}}}^{\leq N}(A_{n,\mathbb Q})\to {\underline{\operatorname{Aut}}}^{\leq N}(P_{n,\mathbb Q})$$

be the family of constructible one-to-one maps compatible with increasing $N$, stabilization in $n$, and the group structure. Constructible bijectivity conjecture. There exists $p_1(n,N)\geq p_0(n,N)$ such that for every prime $p>p_1(n,N)$, the canonical constructible map

$$\phi_{n,N,p}^{\mathrm{can}}:{\underline{\operatorname{Aut}}}^{\leq N}(A_{n,\mathbb Z/p\mathbb Z})\hookrightarrow {\underline{\operatorname{Aut}}}^{\leq N}(P_{n,\mathbb Z/p\mathbb Z})$$

is a bijection. This is presented as a finite-characteristic strengthening of the proposed Weyl–Poisson automorphism correspondence; the supplied source gives no resolution.