A polynomial bound for a logarithm

Let $x=\sqrt{\frac{b}{a}}\ge 1$ and $a^2\ge 1$ then it just need to show: $\frac{2x+\frac{1}{2}+\frac{x^2}{2}}{3}\ge \frac{2\ln x}{x^2-1}\Longleftrightarrow (x^2-1)(x^2+4x+1)-12\ln x\ge 0$

Source: InternLM Lean-Workbook, record lean_workbook_3104 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.