Certified B6 block-pair search terminates

Fix any word and precision inspected by [F3]. For a $d\times d$ complex matrix whose real and imaginary entry coordinates have errors at most $2^{-p}$, summing their squares bounds the Frobenius error by $d\sqrt{2}{2}^{-p}$. The word and target approximants from [F2]--[F3] thus have two errors totaling at most $2d\sqrt{2}{2}^{-p}<3d{2}^{-p}$. The triangle inequality gives $\mathrm{\parallel }{B}_d(b)-T_d{\mathrm{\parallel }}_F\le \mathrm{\parallel }{P}_{d,b,p}-Q_{d,p}{\mathrm{\parallel }}_F+3d{2}^{-p}$.

The product of open operator-norm $\epsilon \mathrm{/}128$-balls around $T_5,T_8$ is a neighborhood in $SU(5)\times SU(8)$. By [A1] and [F1], it meets the normalized B6 image, so there is one finite braid word $b_{\ast }$ with both block operator errors less than $\epsilon \mathrm{/}128$. For dimension $d\le 8$, the real-coordinate ${\mathrm{\ell }}^1$ norm of a complex matrix is at most $\sqrt{2}d\mathrm{\parallel }A{\mathrm{\parallel }}_F\le \sqrt{2}{d}^{3\mathrm{/}2}\mathrm{\parallel }A{\mathrm{\parallel }}_{\mathrm{o}\mathrm{p}}\le 32\mathrm{\parallel }A{\mathrm{\parallel }}_{\mathrm{o}\mathrm{p}}$ by [F4]. Hence the exact coordinate-sum distance in either block is strictly less than $\epsilon \mathrm{/}4$.

The rational sum $s_{d,b,p}$ of absolute real and imaginary coordinates dominates $\mathrm{\parallel }{P}_{d,b,p}-Q_{d,p}{\mathrm{\parallel }}_F$. Hence [F4] gives $\mathrm{\parallel }{B}_d(b)-T_d{\mathrm{\parallel }}_{\mathrm{o}\mathrm{p}}\le s_{d,b,p}+3d{2}^{-p}<s_{d,b,p}+4d{2}^{-p}$. If the corresponding rational test passes, this is strictly below $\epsilon$. Both passing tests therefore certify the two strict block-error bounds without any choice assumption.

Fix this finite word. Its exact block matrices and the targets have coordinate approximants converging to their entries by [F2]–[F3]. Therefore $s_{d,b_{\ast },p}$ converges to the real-coordinate ${\mathrm{\ell }}^1$ distance between the exact word block and target; by step 1.2 that limit is less than $\epsilon \mathrm{/}4$. Since $4d{2}^{-p}\to 0$, some finite $p$ makes both certificates strictly below $\epsilon$. Dovetailing eventually examines $(b_{\ast },p)$, and the return rule [F3] triggers acceptance. Step 2.1 supplies both strict block-error bounds for the returned word. Thus the procedure halts. ACω enters only through [A1] and [F1]; density gives no search-index bound.