What is the proof of the "thin set theorem"? A result in infinite Ramsey theory.

OK so here's a precise question:

Is it true that for every integer $k\geq1$ and every $f:\mathbb{Z}^k\to\mathbb{Z}$, there is some infinite subset $A\subseteq\mathbb{Z}$ such that $f(A^k)$ is not all of $\mathbb{Z}$? Here $A^k$ is the obvious subset of $\mathbb{Z}^k$ consisting of elements all of whose coordinates are in $A$.

This is some delicate question in infinite Ramsey theory. It seems to me that Harvey Friedman knows a lot about this question, and knows various fragments of Peano Arithmetic where this is provable, or not provable, and so on. My understanding is that Friedman calls this "the thin set theorem". But my reading of various bits of Friedman's writing on this subject still leaves me confused about whether this result is provable in what I would call "mathematics" and what he would probably call "ZFC". Can anyone clarify the status of this question in ZFC for me?

I'll follow @ccc's advice and answer my own question by explaining Friedman's argument but giving some more details. I've made it community wiki (for the usual reason: I then won't be seen to gain from answering my own question).

Notation: if $X$ is a set and $n\in\mathbb{Z}_{\geq1}$ then $X^{(n)}$ denotes the set of subsets of $X$ of size $n$.

We start with

The infinite Ramsey Theorem: If $X$ is countably infinite and we colour $X^{(n)}$ with $k\in\mathbb{Z}_{\geq1}$ colours (that is, we give a map $X^{(n)}\to\{1,2,\ldots,k\}$) then there's an infinite monochramatic subset of $X$ (that is, there's some infinite $Y\subseteq X$ such that the induced map $Y^{(n)}\to\{1,2,\ldots,k\}$ is constant).

The proof is short but clever, and is at wikipedia for example. The proof does the case $k=2$ by a clever induction on $n$ and then does the general case by induction on $k$. I'll omit the details.

Clearly this is a result with the same flavour as the thin set theorem, but as ccc points out, this isn't quite what we want because in the thin set theorem we have ordered $k$-tuples, not subsets of size $n$. So we need a minor modification to deal with this. Here's how it goes. Define an equivalence relation on $\mathbf{Z}^k$, called "being of the same order type", thus: say $a=(a_1,a_2,\ldots,a_k)$ and $b=(b_1,b_2,\ldots,b_k)$ are equivalent if for all $1\leq i,j\leq k$ we have $a_i<a_j$ iff $b_i<b_j$ (note that this implies $a_i=a_j$ iff $b_i=b_j$). Clearly there are only finitely many equivalence classes. Say there $p=p(k)$ equivalence classes. We call the equivalence classes "order types".

Now here's Friedman's proof of the thin set theorem. Given $f$ as in the theorem, define $H:\mathbf{Z}^k\to\{1,2,\ldots,p+1\}$ by $H(x)=f(x)$ if $1\leq f(x)\leq p$, and $H(x)=p+1$ otherwise. Now we apply the infinite Ramsey Theorem $p$ times! We first apply it to the colouring of $\mathbf{Z}^{(k)}$ given thus: given a subset of $\mathbf{Z}$ of size $k$, order the elements as $x_1<x_2<\ldots<x_k$. Now colour this set with colour $H((x_1,x_2,\ldots,x_k))$. Applying Ramsey we get an infinite subset $A_1$ of $\mathbf{Z}$ which is monochromatic. Now we apply it to the colouring of $(A_1)^{(k)}$ given thus: given a subset of size $k$ write it as $x_2<x_1<x_3<x_4<\ldots<x_k$ and colour the subset with the colour $H((x_1,x_2,\ldots,x_k))$. We get an infinite subset $A_2$ of $A_1$ which is monochromatic. We continue in this way, applying Ramsey to each order type. For example we might next do the order type $x_1=x_2<x_3<x_4<\ldots$ and we deal with this by colouring $k-1$-tuples of integers by ordering them and repeating the first element and then applying $H$.

The upshot is an infinite subset $A_p$ of the integers with the property that $H(a_1,a_2,\ldots,a_k)$ depends only on the order type of $(a_1,a_2,\ldots,a_k)$. But there are only $p$ order types, and $H$ takes $p+1$ values, so $H$ on $A^k$ is not surjective and hence $f$ isn't either.