Vasc's inequality by a sum of squares

Idea. For cyclic inequalities, AM-GM and Cauchy-Schwarz often fail because the equality cases are strange. A sum-of-squares certificate proves the inequality for *all real* numbers at once.

Identity. Define
$$S_1=a^2-2ab+bc-c^2+ca,\quad S_2=b^2-2bc+ca-a^2+ab,\quad S_3=c^2-2ca+ab-b^2+bc.$$
Direct expansion gives
$$S_1^2+S_2^2+S_3^2=2\Bigl[(a^2+b^2+c^2)^2-3(a^3b+b^3c+c^3a)\Bigr].$$

Conclusion. The left side is a sum of squares, hence $\ge0$, so the inequality holds.

Equality. Iff $S_1=S_2=S_3=0$. Besides $a=b=c$, there are other equality cases of the form $\left(\sin^2\frac{4\pi}7,\sin^2\frac{2\pi}7,\sin^2\frac\pi7\right)$ up to scaling.

Remark. This is Vasile Cîrtoaje's inequality.

Lesson. For a polynomial inequality valid on all of $\mathbb{R}^n$, try to write the difference as a sum of squares (SOS).