The exact greedy computation tracks a Boolean used table and advances a least-missing pointer after every insertion. At term 1,000,000 the pointer equals 523,263. Hence every integer from 1 through 523,262 has appeared. The last term is 1,109,402, and the largest term seen is 1,573,378.

This is an exhaustive statement about the stated prefix. It supplies finite evidence for the permutation question.

Let \(x\) be the current term and choose a set bit \(2^j\) of \(x\). For every bit position \(k\) outside the support of \(x\), the integer \[ y=2^j+2^k \] shares exactly the bit \(2^j\) with \(x\). There are infinitely many choices of \(k\), while only finitely many integers have been used at any finite stage. An unused eligible \(y\) therefore exists, and the well-ordering of the positive integers supplies the least one. The recurrence continues forever. Its explicit unused condition also makes all terms distinct.

This argument settles nontermination and injectivity. Surjectivity requires a separate argument.

OEIS A226077 starts with \(a(1)=1\) and chooses the smallest unused positive integer sharing exactly one 1-bit with its predecessor. This is the candidate recurrence word for word. Paul Tek submitted the entry on May 25, 2013. Reinhard Zumkeller supplied a Haskell generator the following day.

The OEIS b-file contains 10,000 terms. An independent parser compared every one with the direct greedy generator used for this entry. All terms agree. The compact JSON vector has SHA-256 digest `9f2304a259bb7ea43816fe6a1a61e322f67ecfe4fae172219da70034905ce505`; its last term is 10,391 and its maximum is 16,401.

A comment added to OEIS A226077 by Reinhard Zumkeller on May 26, 2013 calls the sequence a permutation and points to A226093 as its inverse. A226093 has the title "Inverse permutation to A226077." The accessible records give definitions, generators, and 10,000-term tables. They contain no proof of surjectivity. The source search for this entry found no paper or later proof resolving the universal claim.

The nearby disjoint-support sequence A109812 has a short surjectivity proof: its first term at least \(2^k\) must equal \(2^k\), which then forces the least missing value. Exact-one overlap breaks that lemma. In A226077, 6 occurs before 4 and 9 occurs before 8. The A109812 proof therefore cannot be copied into this setting.

The million-term certificate moves the verified least missing value to 523,263. A resolution still needs a proof that every least missing value is eventually forced, or a positive integer that remains absent forever.

The trie has one leaf for every integer below \(2^{22}\). Each internal node stores the number of unused leaves beneath it. A query reads candidate bits from most significant to least significant, always tries 0 before 1, and carries a state saying whether the candidate and current term have shared zero or one set bits. A leaf is accepted exactly in state one. This left-first traversal returns the smallest eligible unused leaf. Deleting every chosen leaf enforces distinctness.

Every successful query returns a value below \(2^{22}\). All integers outside the trie are larger, so each returned leaf is also the global greedy minimum. The program checks the defining bit-intersection condition at every step, checks the first 20 terms, and asserts three checkpoints. It also maintains the least missing integer directly. The FNV-1a digests serialize each 32-bit term in little-endian byte order.

The first 10,000 terms agree term by term with the OEIS b-file. Compiled with Apple clang 17.0.0 using `c++ -std=c++17 -O3 -Wall -Wextra -pedantic`, the million-term run took about one second on an Apple Silicon workstation. The stable three-line output has SHA-256 digest `ee795c4535cedea9c942244e3f4731cc2d7b70a6821ef43d6141c92c2172a96c`.