An operator-norm counterexample to the weighted log-majorization

For positive definite $A,B$ and $0\le t\le1$, the conjecture asserts the
log-majorization $s(A^t(A\#_tB)B^{1-t})\prec_{\log}s(AB)$ of singular values,
where $\#_t$ is the weighted geometric mean. The note disproves even the
largest-singular-value inequality: for $A=\operatorname{diag}(256,1/256,1)$,
an explicit integer positive definite $3\times3$ matrix $B$ and $t=1/8$, the
operator norm of $A^{1/8}(A\#_{1/8}B)B^{7/8}$ exceeds $10900$, while
$\|AB\|_2<10200$. The proof replaces the eighth roots of
$A^{-1/2}BA^{-1/2}$ and of $B$ by explicit rational matrices whose eighth
powers lie within $10^{-8}$ of the targets in Frobenius norm, checked in exact
rational arithmetic. The estimate $\|P^\alpha-Q^\alpha\|\le\alpha
m^{\alpha-1}\|P-Q\|$ for $P,Q\ge mI$ and $0<\alpha<1$, from an integral
representation of $x^\alpha$, transfers these bounds to the true roots, and
one entry of the resulting rational product exceeds $11000$.