A product of two binary quadratic forms bounds a squared bilinear form

By AM-GM, we know that $a^2 + 3c^2 \ge 2 \sqrt{3} ac$ $b^2 + 3d^2 \ge 2 \sqrt{3} bd$ Therefore, $2(\sqrt{3})(ac + bd) \le (a^2 + b^2) + 3(c^2 + d^2) = (a - b)^2 + 3(c - d)^2 + 2(ab + 3cd) = 4(a - b)^2 + 4ab = 4(a^2 - ab + b^2)$ Since $a^2 - ab + b^2 = c^2 + cd + d^2$, we get that $\frac{3}{4} (ac + bd)^2 \le (a^2 - ab + b^2)(c^2 + cd + d^2)$

Source: InternLM Lean-Workbook, record lean_workbook_46786 (Apache-2.0). Complete source proposition preserved; proof developed independently.