Words with factor complexity $2n+1$ and minimal critical exponent

Word $\mathbf{G}$ is the fixed point of the morphism $\gamma =[01,2,02]$. In 2019, Shallit and Shur showed that $\mathbf{G}$ has factor complexity $2n+1$. They also showed that $\mathbf{G}$ has critical exponent $\mu =2+\frac{1}{{\lambda }^2-1}=2.4808726\cdots$, where $\lambda =1.7548777$ is the real zero of $x^3-2x+x-1=0$. They conjectured that this was the least possible critical exponent among words with factor complexity $2n+1$. We confirm their conjecture. The proof, using an intricate case analysis, is by computer. The relevant program generates a `human readable’ proof.