A proof of a conjecture of T. Piesk: nim-products of powers of 2 and Stern's diatomic sequence

We prove a conjecture of T. Piesk stated in 2013 in the OEIS entries A002487 (Stern's diatomic sequence) and A223541 (the array of nim-products 2^m ⊗ 2^n): for every n >= 0, the number of distinct values of 2^x ⊗ 2^y with x + y = n equals A002487(n+1), the number of hyperbinary representations of n. Here ⊗ is Conway's nim-multiplication, under which the nonnegative integers form a field of characteristic 2. The proof has three steps. First, writing alpha_k = 2^(2^k) for the Fermat 2-powers, every 2^x is the nim-product of the alpha_k over the binary digits of x, so 2^x ⊗ 2^y depends only on the pair (A, B) of sets of binary positions where exactly one, respectively both, of x and y have a digit 1; such a pair is a hyperbinary representation of n = x + y. Second, and this is the main point, the map (A, B) -> (product of alpha_k over A) ⊗ (product of alpha_k ⊗ alpha_k over B) is injective on pairs of disjoint finite sets: by induction on the largest position t, using that a nimber below 2^(2^(t+1)) splits uniquely into a high half and a low half, which are its coordinates in the basis {1, alpha_t} of GF(2^(2^(t+1))) over GF(2^(2^t)), and that the three situations "t in A", "t in B", "t in neither" leave different patterns of zero and nonzero halves. Third, hyperbinary representations of n are counted by A002487(n+1) (Carlitz, Lind, Reznick; see Northshield). As a corollary we describe all coincidences in the array A223541: 2^m ⊗ 2^n = 2^m' ⊗ 2^n' if and only if m XOR n = m' XOR n' and m AND n = m' AND n', and 2^m ⊗ 2^n = 2^(m XOR n) ⊗ 2^(m AND n) ⊗ 2^(m AND n); on the antidiagonal m + n = N each distinct value occurs exactly 2^(number of ones in m XOR n) times. The proof is elementary and uses only the classical facts about nim-multiplication (Conway, On Numbers and Games, Chapter 6; Lenstra, Nim multiplication, 1978). Its interest lies in the exact count, which connects the arithmetic of nimbers with the arithmetic of binary representations, and in the mechanism it reveals. As of October 5, 2026 the statement was still marked as a conjecture in both OEIS entries, and we have not found a proof in the literature. The note also explains the methodology of the author's project on open statements in the OEIS (translation of the statements into formulas for the reasoning engine SyntheticMind, with time budgets by type of computation; a log of obstacles that decides which methods to implement next; recursive splitting into subgoals; independent verification; an independent referee) and the steps that led to this proof. The use of AI is described in the paper. Files: Blanco_Gomez_2026_Piesk_nim_EN.pdf is the paper; Blanco_Gomez_2026_Piesk_nim_ES.pdf is the Spanish version (same content); verify_piesk.py is the independent verification script (Python, no external libraries; it implements nim-multiplication, checks it against the mex definition for small values, and verifies every lemma, the theorem for n <= 120 and the corollary; it runs in a fraction of a second and prints ALL CHECKS PASSED).