Lemma: An exact zero test

Every element of $\mathcal{R}$ has a representation

Such an element is zero precisely when $a=b=c=d=0$. Accordingly, a finite circuit's bad-output amplitudes admit exact symbolic zero checks.

Proof. The displayed form is closed under addition, multiplication, conjugation, and the generators of $\mathcal{R}$, after enlarging the denominator when necessary. If $\alpha =0$, its real and imaginary parts vanish. Irrationality of $\sqrt{2}$ gives $a=b=0$ and $c=d=0$. The converse is immediate.