Functional equation $f\left(\frac{x+y}{2}\right)+f\left(\frac{2xy}{x+y}\right)=f(x)+f(y)$ implies $2f(\sqrt{xy})=f(x)+f(y)$ Prove that if the function $f$ is defined on the set of positive real numbers, its values are real, and $f$ satisfies the equation
$$f\left( \frac{x+y}{2}\right) + f\left(\frac{2xy}{x+y} \right) =f(x)+f(y)$$
for all positive $x,y$, then
$$2f(\sqrt{xy})=f(x)+f(y)$$
for every pair $x,y$ of positive numbers.

Source: Miklos Schweitzer Memorial Competition 2001

I can see how the repeated application of the functional equation condition upon itself forms a bound, but how can I formally prove this?

Solution modified from here
By repeated application of the function property for some positive reals $a,b,c,d$ as you suggested:
$$\begin{align*}f(a)+f(b)+f(c)+f(d)&= f\left({a+b\over2}\right)+f\left({2ab\over a+b}\right)+f\left({c+d\over2}\right)+f\left({2cd\over c+d}\right) \\ 
&=f\left({{a+b\over2}+{c+d\over2}\over2}\right)+f\left({2{a+b\over2}\cdot{c+d\over2}\over{a+b\over2}+{c+d\over2}}\right)+f\left({{2ab\over a+b}+{2cd\over c+d}\over2}\right)+f\left({2{2ab\over a+b}\cdot{2cd\over c+d}\over{2ab\over a+b}+{2cd\over c+d}}\right) \\ &= f\left({a+b+c+d\over4}\right)+f\left({(a+b)(c+d)\over a+b+c+d}\right)+f\left({abc+abd+acd+bcd\over(a+b)(c+d)}\right)+f\left({4abcd\over abc+abd+acd+bcd}\right) \end{align*}$$Now if we 'swap' $b$ and $c$ and repeat a similar process, one finds $$f\left({(a+b)(c+d)\over a+b+c+d}\right)+f\left({abc+abd+acd+bcd\over(a+b)(c+d)}\right)=f\left({(a+c)(b+d)\over a+b+c+d}\right)+f\left({abc+abd+acd+bcd\over(a+c)(b+d)}\right)\tag{1}$$ Now substitute $a=c$, $b=\frac{a^2}{d}$ and $t=\frac{a}{b}+\frac{b}{a}$ so that $$\frac{(a+b)(c+d)}{ a+b+c+d}=\frac{abc+abd+acd+bcd}{(a+b)(c+d)}=a$$ $${(a+c)(b+d)\over a+b+c+d}=a\cdot{2t\over2+t}$$ and $${abc+abd+acd+bcd\over(a+c)(b+d)}=a\cdot{2+t\over2t}$$ If we substitute these results into $(1)$, we find $$2f(a)=f\left(a\cdot{2t\over2+t}\right)+f\left(a\cdot{2+t\over2t}\right)\tag{2}$$ It can be seen that $t\geq 2$ by AMGM and thus $\frac{2t}{2+t}\geq 1$. Hence for all pairs $x\geq y$ there exist suitable $a$ and $t$ so that $$a\cdot{2t\over2+t}=x,a\cdot{2+t\over2t}=y\text{   and  } \sqrt{xy}=a$$ so that $(2)$, and thus the required property, holds.
