Idempotent ultrafilter ($\mathcal{U}+\mathcal{U}=\mathcal{U}$)

An additive idempotent ultrafilter satisfies $\mathcal{U}+\mathcal{U}=\mathcal{U}$. On positive integers it is necessarily nonprincipal, since a principal ultrafilter at $n$ adds to itself to give the principal ultrafilter at $2n$. The idempotent-ultrafilter star-set lemma converts this algebraic property into a recursive construction of finite sums. If zero is included, the trivial principal idempotent at zero must be excluded for that increasing-sequence application.

For $A\in \mathcal{U}$ and an idempotent ultrafilter, put $A^{\ast }=\{n\in A:A-n\in \mathcal{U}\}$. Then $A^{\ast }\in \mathcal{U}$, and $A^{\ast }-n\in \mathcal{U}$ for every $n\in A^{\ast }$. For the second assertion, apply idempotence to $A-n$ and intersect its resulting good-translation set with $A-n$. This allows each new finite-sums generator to be chosen from finitely many translation constraints, proving the Idempotent-ultrafilter proof of Hindman's theorem.