>>2
結構単純な証明を思いついたが…。

Z^2の代わりにZ[i]を使う。またε, ε_1, ...をZ[i]の単数をあらわす変数とする。
f:Z[i]→Rがf≧0, 4*f(m+ni) = 農{k=0, 1, 2, 3} f(m+ni+i^k) を満たすとする。
このとき、農{k=0, 1, 2, 3}（f(m+ni)-f(m+ni+i^k)）=0.
よってf(m+ni)≠f(m+ni+ε)ならば、あるε_1があってf(m+ni)>f(m+ni+ε_1)となる。
f(m+ni+ε_1)について同様の考察を行うと、
f(m+ni+ε_1)>f(m+ni+ε_1+ε_2)を満たすε_2を得る。
以下同様にして
f(m+ni)>f(m+ni+ε_1)>f(m+ni+ε_1+ε_2)>...>f(m+ni+ε_1+ε_2+...+ε_l)>...
となる無限列を得るが、これはf≧0に反する。(Q. E. D)

ちなみに一般にZ^2の代わりにGを加群、AをGの対称な部分集合として、
4*f(n, m)=f(m-1, n)+f(m+1, n)...の代わりに|A|*f(g)=農{a∈A}f(g+a)を条件としても
上の証明と同様にして対応する結果を導ける。