An approach that should work is to derive the differential equation that any minimizer would have to satisfy and check that its solutions are the known ones for which equality holds. To fill in the details, one would need to show that a minimizer does exist and has the necessary regularity to make the derivation of the differential equation valid, but I think that such arguments are standard in the calculus of variations and should be applicable here.

So, *assume that a minimizer $f$ exists* and set
$$
a = \frac1{2\pi}\int_0^{2\pi}\cos f(x)\,dx\quad\text{and}\quad
b = \frac1{2\pi}\int_0^{2\pi}\sqrt{f'(x)^2+\sin^2 f(x)}\ dx.
$$
Note that, if $b=0$, then $f(x)$ is an integer multiple of $\pi$ and we have equality. Set this case aside and assume that $b>0$. The assumption that $f$ be a minimizer implies that if $u$ is any $2\pi$-periodic function then $I'(0)=0$ where
$$
\begin{align}
I(t) &= \left(\int_0^{2\pi}\cos\bigl(f(x){+}tu(x)\bigr)\,dx\right)^2\\
&\qquad\qquad+\left(\int_0^{2\pi}\sqrt{(f'(x){+}tu'(x))^2+\sin^2 (f(x){+}tu(x)\bigr)}\ dx\right)^2.
\end{align}
$$
Calculation (using integration by parts and the fact that $u$ and $f$ can be regarded as $2\pi$-periodic) then yields that $I'(0)/(4\pi)$ equals
$$
\int_0^{2\pi} \left(-b\left(\frac{f'(x)}{\sqrt{f'(x)^2{+}\sin^2 f(x)}}\right)'+\frac{b\sin f(x)\cos f(x)}{\sqrt{f'(x)^2{+}\sin^2 f(x)}}-a\sin f(x)\right)\,u(x)\ dx.
$$
Consequently, setting $\lambda = a/b$, we have that $f$ must satisfy a second-order differential equation with parameter $\lambda$
$$
\left(\frac{f'(x)}{\sqrt{f'(x)^2{+}\sin^2 f(x)}}\right)'-\frac{\sin f(x)\cos f(x)}{\sqrt{f'(x)^2{+}\sin^2 f(x)}}+\lambda\,\sin f(x) = 0.\tag1
$$
Thus, there is a $3$-parameter family of solutions to this equation with parameter, and $f$ must belong to this $3$-parameter family.

Now, it just so happens that we already know a $3$-parameter family of solutions to this equation, namely
$$
f(x) = \arccos\left(\frac{u{+}(p\cos x {+} q \sin x)\sqrt{(p\cos x {+} q \sin x)^2+1-u^2}}{1{+}(p\cos x {+} q \sin x)^2}\right),
\tag2
$$
where $|u|<1$ and $p$ and $q$ are $3$ real numbers, and all of these solutions $f$ give $a^2+b^2 = 1$, i.e., equality in the desired inequality. One gets other $3$-parameter families by adding an integer multiple of $\pi$ to the above formula, but these can be considered equivalent. It turns out that this then gives all of the solutions except the ones that have $\sin f(x) \equiv 0$. (Allowing $|u|\ge1$ gives families of solutions that can be defined only over subintervals of $[0,2\pi]$, and these must be taken into account in the analysis as well.)

Again, in order to make this argument fully rigorous, one has to prove that a minimizer does exist in the first place and prove a regularity result for solutions of the above ODE at places where $\sin f(x)$ vanishes. I think that those are doable, but I haven't checked the details.

anycircle on the sphere, then equality holds. Thus, there is (at least) a $3$-parameter family of functions $f$ that give equality, while the case of constant $f$ only constitutes a $1$-parameter family. $\endgroup$ – Robert Bryant Jan 23 at 13:26