Kac's Walk on Rotation Matrices Mixes in $\boldsymbol{Θ(n^2)}$ Steps: A Proof Discovered with AI

Let $N=\binom n2=\dim\mathrm{SO}(n)$. We prove that the coordinate-plane Kac walk on $\mathrm{SO}(n)$ has total-variation mixing time of order $N$: for every fixed $0<\varepsilon<1$, \[ t_{\mathrm{mix}}^{(n)}(\varepsilon)=Θ_\varepsilon(n^2). \] The lower bound is the dimensional singularity obstru