The Binary Two-Up Sequence

The Binary Two-Up Sequence is the lexicographically earliest sequence of distinct nonnegative integers with the property that the binary expansion of the n-th term has no 1-bits in common with any of the previous floor(n/2) terms. We show that the sequence can be decomposed into ``atoms'', which are sequences of 4, 6, or 8 numbers whose binary expansions match certain patterns, and that the sequence is the limiting form of a certain ``word'' involving the atoms. This leads to a fairly explicit formula for the terms, and in particular establishes the conjecture that every nonzero term is the sum of at most two powers of 2.