 All-black red-black tree size criterion

A red-black tree with no red stored nodes is a perfect binary tree. Indeed, every root-to-sentinel path has equal length because every real node is black; a missing branch at an earlier level would make its path shorter. Thus every real level is full. Its size is $2^h-1$ for some number $h$ of real levels. Conversely, colouring every stored node of a perfect binary tree black satisfies every red-black invariant. This proves both directions of the size criterion.