Labelling binary trees by powers of two

Gro-Tsen asked on MathOverflow (question 304266, 2018) whether every rooted tree with n vertices, each vertex having at most two children, can be labelled by 0, 1, …, n − 1 so that the root gets 0 and every child exceeds its parent by a power of two. The question is open. This note collects what is known.

• Theorem 1. A tree is labelled whenever smaller trees are and one of five shapes occurs at the root: a single child; branch sizes equal or differing by one; a branch of size 2^k − 1; a branch that is a chain of d vertices above a subtree, with d + 1 or d + 2 a power of two and sizes matched; two such chains. John Machacek’s MathOverflow answer has the equal-size and 2^k − 1 cases.
• Lemmas 2 and 3, Corollary 4. Call a label set universal if every tree of its size can be labelled onto it. A universal set has a universal tail ({s − p} for its least positive element p, a power of two), and primitive universal sets lie in [0, 2^(n−2)]. So the universal sets are generated, exactly, by lifting smaller ones; the family is irregular (sporadic members at sizes 4, 5, 6, 8, 9, 14 and 16 to 21).
• Proposition 5. Every tree with at most 24 vertices is labelled (34,504,201 trees); every tree with at most 22 vertices can have its root’s children labelled 1 and 2; the primitive universal sets of size at most 21 are listed; and from 11 vertices on, no proof can label the two branches by fixed universal sets chosen from the branch sizes alone.

Preprint, 10 October 2026, not peer reviewed. Theorem 1, Lemmas 2 and 3 and Corollary 4 are formally verified in Lean 4 (lean/, standard axioms only). The exposition has not yet been independently reviewed. The author used AI tools (Claude, Anthropic; Codex, OpenAI) in this work, as described in the note’s acknowledgements, and is responsible for its content.