Clifford+T denominator descent and finite base table

For a nonzero real element $P+\sqrt{2}Q\in \mathbb{Z}[\sqrt{2}]$, define $\nu (P+\sqrt{2}Q)$ as the largest $r\ge 0$ for which $(\sqrt{2}{)}^r$ divides it in $O$. This maximum exists: divisibility by $(\sqrt{2}{)}^{2q}=2^q$ forces both integer coefficients $P,Q$ to be divisible by $2^q$, which cannot hold for arbitrarily large $q$ unless the element is zero. If $y=(\sqrt{2}{)}^j{y}_0$ with $\sqrt{2}\nmid y_0$, then the definition of sde gives $\mathrm{sde}(y\mathrm{/}(\sqrt{2}{)}^r)=r-j$.

Applying each embedding of $K$ to $\mathrm{\mid }u{\mathrm{\mid }}^2+\mathrm{\mid }v{\mathrm{\mid }}^2=1$ preserves the identity by [F6]; hence every embedding of each entry has modulus at most $1$. Since $s>3$, $u\mathrm{\ne }0$. If $v=0$, then $\mathrm{\mid }u{\mathrm{\mid }}^2=1$ and $s=0$, a contradiction, so $v\mathrm{\ne }0$ as well. Let $r_u=\mathrm{sde}(u)$ and $r_v=\mathrm{sde}(v)$. From [F2] and $s>3$, $r_u\ge 2$. More generally, if $\max (r_u,r_v)\ge 1$ and the exponents differ, the same argument below gives a contradiction. If $r_u>r_v$, set $x=(\sqrt{2}{)}^{r_u}u$ and $y=(\sqrt{2}{)}^{r_v}v$. Then $x\bar{x}+2^{r_u-r_v}y\bar{y}=2^{r_u}$; the right side and second term lie in $2O$, so $x\bar{x}\in 2O$. Write $x=a_0+a_1\omega +a_2{\omega }^2+a_3{\omega }^3$. By [F3], $x\bar{x}=P+\sqrt{2}Q$ with $P=\sum a_j^2$ and $Q=a_0(a_1-a_3)+a_2(a_1+a_3)$. If $P,Q$ are both even, then $a_0+a_2$ and $a_1+a_3$ have equal parity because $P\equiv (a_0+a_2)+(a_1+a_3)(\mathrm{m}\mathrm{o}\mathrm{d}2)$, while $Q\equiv (a_0+a_2)(a_1+a_3)(\mathrm{m}\mathrm{o}\mathrm{d}2)$ forces both even. Then [F3] gives $\sqrt{2}\mid x$, contradicting the minimality of $r_u$. Since $x\bar{x}\in 2O$ would make both $P,Q$ even in the power basis, this is impossible. If $r_v>r_u$, interchange $u,v$ and use the same calculation with the larger exponent. Thus $r_u=r_v=:r$. Write $x=(\sqrt{2}{)}^{r}u$ and $y=(\sqrt{2}{)}^{r}v$. Their minimal exponents make both primitive with respect to $\sqrt{2}$. The same parity argument shows $x\bar{x}$ and $y\bar{y}$ are not divisible by $2$, so their divisibility by $\sqrt{2}$ is either zero or one. Since $r\ge 2$, $x\bar{x}+y\bar{y}=2^r$ is divisible by $\sqrt{2}$; exactly one of the two norms cannot be divisible by $\sqrt{2}$, since then their sum would not be divisible by it. Hence $\nu (x\bar{x})=\nu (y\bar{y})=j\in \{0,1\}$. Also $r\ge 0$ by [F4], since the entries and their $\bullet$-conjugates are all in the unit disk.

The squared-entry identity [F2] gives $s=2r-j$. If $r\ge 3$, then $x\bar{x}+y\bar{y}=2^r$, so the integer forms $P(x),Q(x),P(y),Q(y)$ satisfy $P(x)+P(y)\equiv Q(x)+Q(y)\equiv 0(\mathrm{m}\mathrm{o}\mathrm{d}8)$. For a real element $P+\sqrt{2}Q$, direct successive division by $\sqrt{2}$ gives $\nu \ge 1⟺2\mid P$, $\nu \ge 2⟺2\mid P,Q$, $\nu \ge 3⟺4\mid P$ and $2\mid Q$, and $\nu \ge 4⟺4\mid P,Q$. These tests depend only on the four coefficients modulo $8$ for every requested exponent through $4$. The finite checker enumerates all $4096$ vectors in $(\mathbb{Z}\mathrm{/}8{)}^4$, groups the $3072$ vectors with $\nu =0$ or $1$, and checks all $393216$ compatible residue pairs. For every pair and each $d=1,2,3$, it finds a $k\in \{0,1,2,3\}$ with $\nu (\mathrm{\mid }x+{\omega }^{-k}y{\mathrm{\mid }}^2)=j+d$; all $1,179,648$ negative-power targets pass. Taking $d=3$ yields $\mathrm{sde}(\mathrm{\mid }(u+{\omega }^{-k}v)\mathrm{/}\sqrt{2}{\mathrm{\mid }}^2)=2(r+1)-(j+3)=s-1$. The same code checks the positive-power form as a cross-check.

The only remaining case with $s>3$ is $r=2,j=0$, so $s=4$. Here $x=2u,y=2v$ satisfy $\mathrm{\mid }x{\mathrm{\mid }}^2+\mathrm{\mid }y{\mathrm{\mid }}^2=4$. The four embedding bounds and Fourier coefficient formula in [F4] give $\mathrm{\mid }{x}_i\mathrm{\mid },\mathrm{\mid }{y}_i\mathrm{\mid }\le 2$. The checker therefore exhausts all integral coefficient vectors in $[-2,2{]}^4$ for both columns, retains the $256$ normalized pairs with $\nu (\mathrm{\mid }x{\mathrm{\mid }}^2)=0$, and verifies for each a $k\in \{0,1,2,3\}$ that $\mathrm{sde}(\mathrm{\mid }(x+{\omega }^{-k}y)\mathrm{/}(\sqrt{2}{)}^3{\mathrm{\mid }}^2)=3$. This proves descent at the boundary $s=4$.

Suppose $s\le 3$. If $u\mathrm{\ne }0$, [F2] gives $\mathrm{sde}(u)\le 2$; if $u=0$, its assigned exponent is $-\mathrm{\infty }$. If $v=0$, the unit-circle result [F7] gives $u={\omega }^j$, so its power-basis coefficients have absolute value at most $1$. If $u=0$, [F7] gives $v={\omega }^j$, with the same coefficient bound. In the remaining case both entries are nonzero. The embedding bounds from step 1.2 and [F4] give nonnegative exponents for both. If either exponent is positive, the unequal-exponent contradiction in step 1.2 forces them equal, so both are at most $2$; if neither is positive, both are $0$. Thus [F4] bounds every numerator coefficient by $2$. The exact enumeration in the certificate contains all such columns: it finds $1537$ possible entries and exactly $208$ normalized columns, with squared-entry exponents $-\mathrm{\infty },0,2,3$ occurring $8,8,64,128$ times. Exact breadth-first search from $(1,0)$ using $H,T,T^{†}$ reaches every one of the $208$ columns; the stored shortest words have maximum length $16$ and the search visits $7660$ states. Every stored word is re-evaluated by exact rational coefficient arithmetic. Therefore the table prepares every base column.

The certificate is generated by the exact arithmetic program research/quantum-computing-algorithms-60-2026-10-15-batch-13-finite-certificates.py; the complete rows and all residue/boundary counts are in the adjacent JSON. The bounds in step 2.1 and step 2.2 and step 2.3 prove the enumerated finite sets contain every required case, so the checks prove the descent and base assertions rather than sampling them.