[seqfan] Injectivity of a(n) = n^2 - XOR(n^2, n)

[David Radcliffe]

Sequence A174375 <https://oeis.org/A174375> is defined by the equation a(n)
= n^2 - XOR(n^2, n), where XOR is bitwise exclusive OR. (In other words,
XOR is binary addition without carries.)

Computer experiments suggest that this sequence is injective. In fact,
there are no repeated values among the first 10^8 terms. This is quite
surprising to me, because it doesn't "look" injective -- the graph
resembles a Sierpinski triangle on its side.

Can anyone prove that this sequence is injective?

- David Radcliffe