[proofplan] We construct the desired symbol by cutting off the $j$th term near $\xi=0$ at a radius tending to infinity, so that for each fixed compact region in phase space only finitely many modified terms are visible. The cutoff radii are chosen inductively so that the modified high-index terms are small in a prescribed finite list of symbol seminorms. This gives a smooth locally finite sum and lets us estimate each asymptotic remainder in the appropriate symbol class. The uniqueness statement follows directly from the definition of asymptotic expansion and from the fact that $m_N \to -\infty$. [/proofplan]

[step:Enumerate the local symbol seminorms on compact subsets of $U$] Choose an increasing sequence $(K_\ell)_{\ell=1}^{\infty}$ of compact subsets of $U$ such that \begin{align*} K_\ell \subset K_{\ell+1}^{\circ} \end{align*} for every $\ell \in \mathbb{N}$ and \begin{align*} U = \bigcup_{\ell=1}^{\infty} K_\ell. \end{align*} For a compact set $K \subset U$, multiindices $\alpha,\beta \in \mathbb{N}_0^n$, a real number $m \in \mathbb{R}$, and a smooth function $c: U \times \mathbb{R}^n \to \mathbb{C}$, define the local symbol seminorm \begin{align*} p_{K,\alpha,\beta}^{m}(c) := \sup_{(x,\xi) \in K \times \mathbb{R}^n} \langle \xi \rangle^{-m+|\beta|} |\partial_x^\alpha \partial_\xi^\beta c(x,\xi)| \end{align*} where \begin{align*} \langle \xi \rangle := (1+|\xi|^2)^{1/2}. \end{align*} The definition of $S^m_{1,0}(U \times \mathbb{R}^n)$ says precisely that $p_{K,\alpha,\beta}^{m}(c)<\infty$ for all such $K,\alpha,\beta$. For each $q \in \mathbb{N}$, let $\mathcal{P}_q$ denote the finite family of seminorms \begin{align*} \mathcal{P}_q := \{p_{K_\ell,\alpha,\beta}^{m_\ell} : 1 \leq \ell \leq q,\ |\alpha| \leq q,\ |\beta| \leq q\}. \end{align*} These finite families exhaust all seminorms relevant to the orders $m_\ell$. [/step]

[step:Choose cutoffs whose differentiated tails are small in prescribed seminorms]Let \begin{align*} \chi: \mathbb{R}^n \to [0,1] \end{align*} be a smooth function such that $\chi(\eta)=0$ for $|\eta|\leq 1$ and $\chi(\eta)=1$ for $|\eta|\geq 2$. For each $\varepsilon \in (0,1]$ and $j \in \mathbb{N}\cup\{0\}$, define the cutoff-modified symbol \begin{align*} b_{j,\varepsilon}: U \times \mathbb{R}^n \to \mathbb{C}, \qquad b_{j,\varepsilon}(x,\xi) := \chi(\varepsilon \xi)a_j(x,\xi). \end{align*} We claim that for every $j \geq q$, every seminorm $p \in \mathcal{P}_q$, and every $\delta>0$, there exists $\varepsilon_{j,q,\delta}\in (0,1]$ such that \begin{align*} p(b_{j,\varepsilon}) \leq \delta \end{align*} whenever $0<\varepsilon \leq \varepsilon_{j,q,\delta}$. Indeed, fix $p=p_{K_\ell,\alpha,\beta}^{m_\ell}\in \mathcal{P}_q$ with $\ell \leq q \leq j$. By Leibniz's rule, each derivative $\partial_x^\alpha\partial_\xi^\beta b_{j,\varepsilon}$ is a finite sum of terms \begin{align*} \varepsilon^{|\gamma|}(\partial^\gamma \chi)(\varepsilon \xi)\partial_x^\alpha\partial_\xi^{\beta-\gamma}a_j(x,\xi) \end{align*} where $\gamma \leq \beta$. If $\gamma=0$, the factor $\chi(\varepsilon \xi)$ is supported where $|\xi|\geq \varepsilon^{-1}$. Since $a_j \in S^{m_j}_{1,0}$ and $m_j<m_\ell$, this contribution is bounded by a constant multiple of \begin{align*} \sup_{|\xi|\geq \varepsilon^{-1}}\langle \xi \rangle^{m_j-m_\ell}. \end{align*} This tends to $0$ as $\varepsilon\downarrow 0$. If $\gamma\neq 0$, the factor $(\partial^\gamma\chi)(\varepsilon\xi)$ is supported where \begin{align*} \varepsilon^{-1}\leq |\xi|\leq 2\varepsilon^{-1}. \end{align*} On this support, $\varepsilon^{|\gamma|}\langle \xi\rangle^{|\gamma|}$ is bounded independently of $\varepsilon$, and the same inequality $m_j<m_\ell$ gives a bound tending to $0$ as $\varepsilon\downarrow 0$. Since only finitely many $\gamma$ occur, the seminorm tends to $0$. Thus, for each $j \in \mathbb{N}\cup\{0\}$, choose $\varepsilon_j \in (0,1]$ so small that \begin{align*} p(\chi(\varepsilon_j\xi)a_j) \leq 2^{-j} \end{align*} for every $q\leq j$ and every $p\in \mathcal{P}_q$.[/step]

[guided]The purpose of the cutoff is to remove the $j$th symbol near $\xi=0$, but farther and farther out as $j$ increases. Define \begin{align*} b_{j,\varepsilon}: U \times \mathbb{R}^n \to \mathbb{C}, \qquad b_{j,\varepsilon}(x,\xi) := \chi(\varepsilon \xi)a_j(x,\xi). \end{align*} When $\varepsilon$ is small, the condition $\chi(\varepsilon\xi)\neq 0$ forces $|\xi|\geq \varepsilon^{-1}$, so the symbol is only visible at large frequencies. Fix one seminorm \begin{align*} p_{K_\ell,\alpha,\beta}^{m_\ell}(b_{j,\varepsilon}) = \sup_{(x,\xi)\in K_\ell\times\mathbb{R}^n}\langle\xi\rangle^{-m_\ell+|\beta|}|\partial_x^\alpha\partial_\xi^\beta b_{j,\varepsilon}(x,\xi)|. \end{align*} Assume $\ell\leq j$. This is exactly the case in which the order of $a_j$ is strictly below the order $m_\ell$, because $m_j<m_\ell$. Differentiating $b_{j,\varepsilon}$ by Leibniz's rule gives finitely many terms of the form \begin{align*} \varepsilon^{|\gamma|}(\partial^\gamma\chi)(\varepsilon\xi)\partial_x^\alpha\partial_\xi^{\beta-\gamma}a_j(x,\xi) \end{align*} with $\gamma\leq\beta$. If $\gamma=0$, no derivative hits the cutoff. The cutoff only tells us that the term is supported where $|\xi|\geq\varepsilon^{-1}$. Since $a_j$ has order $m_j$, there is a finite constant $C$ such that \begin{align*} |\partial_x^\alpha\partial_\xi^\beta a_j(x,\xi)|\leq C\langle\xi\rangle^{m_j-|\beta|} \end{align*} for $(x,\xi)\in K_\ell\times\mathbb{R}^n$. Multiplying by the weight from the seminorm gives \begin{align*} \langle\xi\rangle^{-m_\ell+|\beta|}|\partial_x^\alpha\partial_\xi^\beta a_j(x,\xi)|\leq C\langle\xi\rangle^{m_j-m_\ell}. \end{align*} Because $m_j-m_\ell<0$, this tends uniformly to $0$ on the region $|\xi|\geq\varepsilon^{-1}$ as $\varepsilon\downarrow0$. If $\gamma\neq0$, a derivative has hit the cutoff. Then $(\partial^\gamma\chi)(\varepsilon\xi)$ is supported in the annulus \begin{align*} \varepsilon^{-1}\leq |\xi|\leq 2\varepsilon^{-1}. \end{align*} The factor $\varepsilon^{|\gamma|}$ from the chain rule is balanced by the annular relation $|\xi|\asymp \varepsilon^{-1}$, so $\varepsilon^{|\gamma|}\langle\xi\rangle^{|\gamma|}$ stays bounded independently of $\varepsilon$. The remaining symbol estimate again leaves the decaying factor $\langle\xi\rangle^{m_j-m_\ell}$, which tends uniformly to $0$ on the annulus as $\varepsilon\downarrow0$. Since each seminorm involves only finitely many derivatives of the cutoff, all contributions tend to $0$. Therefore we may choose $\varepsilon_j$ so small that the modified term $\chi(\varepsilon_j\xi)a_j$ is at most $2^{-j}$ in every seminorm from the first $j$ finite families.[/guided]

[step:Define the asymptotic sum as a locally finite smooth series] For each $j\in\mathbb{N}\cup\{0\}$, define \begin{align*} b_j: U\times\mathbb{R}^n\to\mathbb{C}, \qquad b_j(x,\xi):=\chi(\varepsilon_j\xi)a_j(x,\xi). \end{align*} Now define \begin{align*} a: U\times\mathbb{R}^n\to\mathbb{C}, \qquad a(x,\xi):=\sum_{j=0}^{\infty} b_j(x,\xi). \end{align*} This sum is locally finite in $\xi$: for a fixed compact set $L\subset \mathbb{R}^n$, the condition $b_j(x,\xi)\neq0$ for some $\xi\in L$ implies \begin{align*} \varepsilon_j^{-1}\leq \sup_{\xi\in L}|\xi|. \end{align*} Since $\varepsilon_j\downarrow0$ after passing to a smaller sequence if necessary, only finitely many $j$ satisfy this condition. Hence the sum defines a smooth function on $U\times\mathbb{R}^n$. Moreover, $a\in S^{m_0}_{1,0}(U\times\mathbb{R}^n)$. Indeed, for any compact $K\subset U$ and multiindices $\alpha,\beta$, choose $q$ such that $K\subset K_q$, $|\alpha|\leq q$, and $|\beta|\leq q$. Then $p_{K,\alpha,\beta}^{m_0}$ is dominated by a constant multiple of a seminorm in $\mathcal{P}_q$, because $m_0\geq m_q$. The finitely many terms $b_0,\dots,b_{q-1}$ lie in $S^{m_0}_{1,0}$, and the tail $\sum_{j=q}^{\infty}b_j$ converges absolutely in the corresponding seminorm by the choice $p(b_j)\leq2^{-j}$. Thus $p_{K,\alpha,\beta}^{m_0}(a)<\infty$. [/step]

[step:Estimate the remainder after subtracting the first $N$ symbols] Fix $N\in\mathbb{N}\cup\{0\}$. We must prove \begin{align*} a-\sum_{j=0}^{N-1}a_j \in S^{m_N}_{1,0}(U\times\mathbb{R}^n). \end{align*} Decompose the remainder as \begin{align*} a-\sum_{j=0}^{N-1}a_j=\sum_{j=0}^{N-1}(\chi(\varepsilon_j\xi)-1)a_j+\sum_{j=N}^{\infty}b_j. \end{align*} For $j<N$, the factor $\chi(\varepsilon_j\xi)-1$ is supported where $|\xi|\leq2\varepsilon_j^{-1}$. Hence $(\chi(\varepsilon_j\xi)-1)a_j$ has compact support in the $\xi$ variable. Since it is smooth in $(x,\xi)$ and all $\xi$-derivatives are supported in a fixed compact subset of $\mathbb{R}^n$, it belongs to $S^{-\infty}(U\times\mathbb{R}^n)$, and therefore to $S^{m_N}_{1,0}(U\times\mathbb{R}^n)$. For the infinite tail, fix a compact $K\subset U$ and multiindices $\alpha,\beta$. Choose $q\geq N$ such that $K\subset K_q$, $|\alpha|\leq q$, and $|\beta|\leq q$. For every $j\geq q$, the seminorm $p_{K_q,\alpha,\beta}^{m_N}$ belongs to $\mathcal{P}_q$ up to replacing the index $\ell=N$ in the order by $m_N$, and the construction gives absolute summability of the corresponding seminorms of $b_j$. The finitely many terms $b_N,\dots,b_{q-1}$ lie in $S^{m_N}_{1,0}$ because $m_j\leq m_N$ for $j\geq N$. Therefore \begin{align*} \sum_{j=N}^{\infty}b_j \in S^{m_N}_{1,0}(U\times\mathbb{R}^n). \end{align*} Combining the finite smoothing correction with the tail estimate gives the required remainder estimate. [/step]

[step:Conclude uniqueness modulo smoothing symbols] Let $a,b\in S^{m_0}_{1,0}(U\times\mathbb{R}^n)$ both satisfy \begin{align*} a\sim \sum_{j=0}^{\infty}a_j \end{align*} and \begin{align*} b\sim \sum_{j=0}^{\infty}a_j. \end{align*} By the definition of asymptotic expansion, for every $N\in\mathbb{N}\cup\{0\}$, \begin{align*} a-\sum_{j=0}^{N-1}a_j\in S^{m_N}_{1,0}(U\times\mathbb{R}^n) \end{align*} and \begin{align*} b-\sum_{j=0}^{N-1}a_j\in S^{m_N}_{1,0}(U\times\mathbb{R}^n). \end{align*} Subtracting these two remainders gives \begin{align*} a-b\in S^{m_N}_{1,0}(U\times\mathbb{R}^n) \end{align*} for every $N$. Since $m_N\to-\infty$, membership in all the classes $S^{m_N}_{1,0}$ implies membership in every $S^M_{1,0}$ with $M\in\mathbb{R}$. Indeed, given $M\in\mathbb{R}$, choose $N$ such that $m_N\leq M$; then \begin{align*} S^{m_N}_{1,0}(U\times\mathbb{R}^n)\subset S^M_{1,0}(U\times\mathbb{R}^n). \end{align*} Therefore \begin{align*} a-b\in \bigcap_{M\in\mathbb{R}}S^M_{1,0}(U\times\mathbb{R}^n)=S^{-\infty}(U\times\mathbb{R}^n). \end{align*} This proves uniqueness modulo smoothing symbols and completes the proof. [/step]