Red-Black Tree, in depth: the five properties, the height proof and an invariant checker

The five properties

The standard statement (the one used in CLRS) treats every missing child as a black sentinel leaf, usually called NIL. With that convention a red-black tree is a binary search tree in which:

1. Colour. Every node is red or black.
2. Root. The root is black.
3. Leaves. Every NIL leaf is black.
4. Red rule. A red node has two black children, so no path contains two reds in a row.
5. Black rule. For each node, every path from it down to a NIL leaf contains the same number of black nodes.

The number in property 5, counted from a node x down to the leaves and not counting x itself, is the black-height bh(x). Property 5 is what makes bh(x) well defined: if paths disagreed there would be no single number to call the black-height.

Read the list as two groups. Properties 1 and 3 are bookkeeping: they make colour total and give the leaves a definite colour so that counting works. Property 2 is a normalisation. Properties 4 and 5 are the two that carry the balance guarantee, and every rotation and recolouring in the insert and delete algorithms exists to restore one of them.

Why the properties bound the height

The height bound follows from two short lemmas.

Lemma 1: a subtree rooted at x has at least 2^bh(x) - 1 internal nodes. By induction on height. A NIL leaf has bh = 0 and 2⁰ - 1 = 0 internal nodes. An internal node x has two children, each with black-height bh(x) if the child is red or bh(x) - 1 if it is black, so each child subtree holds at least 2^bh(x)-1 - 1 nodes. Add both children and x itself: 2(2^bh(x)-1 - 1) + 1 = 2^bh(x) - 1.

Lemma 2: bh(root) is at least h/2. On the longest path, of length h, the red rule forbids two reds in a row, so at least half of the nodes below the root are black.

Combine them: n is at least 2^h/2 - 1, so h is at most 2 log₂(n+1).

Put numbers on it. For one million keys, log₂(1,000,001) is about 19.93, so no search ever visits more than 39 nodes. A perfectly balanced tree would need 20 levels; an AVL tree is bounded by roughly 1.44 log₂(n+2), about 28. Red-black trees accept a looser height in exchange for cheaper updates: an insert performs at most two rotations and a delete at most three, while recolouring can travel up the tree but only flips bits. That trade is why the structure is the usual default for ordered maps where writes are frequent.

Check the minimum from the other side too. With black-height 3 a tree needs at least 7 internal nodes, and the tallest tree of black-height 3 alternates black and red on one path to reach height 6. Property 4 lets a path at most double; property 5 stops any path from being short of blacks. Each alone is useless.

Drop one property and see what breaks

A good way to understand an invariant is to delete it and see what survives.

The last two rows are the point. Each of the two load-bearing rules is trivially satisfiable by a terrible tree on its own. Only the pair forces balance, because property 5 equalises the black skeleton and property 4 limits how much red padding can be inserted into any single path.

Variants change the rules on purpose. The left-leaning red-black tree (LLRB, Sedgewick, 2008) adds one: a red node may only be a left child. That removes half of the symmetric cases and, in its common form, makes the tree a binary encoding of a 2-3 tree instead of a 2-3-4 tree. AA trees impose the mirror-image restriction (red links may only lean right), written as levels. Relaxed and chromatic trees go the other way, temporarily allowing violations so that concurrent writers can defer rebalancing.

The 2-3-4 tree behind the colours

The 2-3-4 view explains every case in the algorithms. Group each black node with its red children: zero, one or two red children give a node with one, two or three keys, which is a 2-node, 3-node or 4-node of a B-tree of order 4. The red rule says a red node is never grouped with another red, so groups never exceed three keys. The black rule says every leaf of the B-tree sits at the same depth, which is the defining property of a B-tree. Black-height is the B-tree's height.

Now replay insertion. A new key is coloured red, which leaves every black count unchanged, so property 5 cannot break; only property 4 can. In B-tree terms, the red key joins an existing node. If that node had room, either it is already fine or a rotation reorders the three keys inside one group. If the node was already a 4-node, the red-red violation is an overflow, and recolouring (the parent and uncle go black, the grandparent goes red) is a B-tree split: the middle key moves up to the parent group, which may overflow in turn. That is why the recolouring case can propagate to the root and the rotation cases cannot.

Deletion is the mirror image. Removing a black node shortens some paths by one black, which in B-tree terms is an underflow, fixed by borrowing from a sibling group (rotation) or merging with it (recolouring, which can propagate). Once you see the groups, the famous case tables become ordinary B-tree maintenance written with colours.

Checking the properties in code

Because the properties are local and countable, you can verify a tree in one O(n) traversal. A checker like this belongs in every red-black implementation's test suite; run it after each operation in randomised tests. It also checks BST order and a subtree-size augmentation, discussed below.

RED, BLACK = True, False

class Node:
    __slots__ = ("key", "left", "right", "color", "size")
    def __init__(self, key, color=RED):
        self.key, self.left, self.right = key, None, None
        self.color, self.size = color, 1

def is_red(n):
    return n is not None and n.color == RED      # None plays the black NIL leaf

def size(n):
    return n.size if n else 0

def check(root, left_leaning=False):
    """Return the black-height of a valid tree; raise AssertionError naming the broken property."""
    assert not is_red(root), "property 2: root must be black"
    def walk(n, lo, hi):
        if n is None:
            return 0                                 # NIL leaves are black, bh = 0
        assert (lo is None or lo < n.key) and (hi is None or n.key < hi), f"BST order at {n.key}"
        if is_red(n):
            assert not is_red(n.left) and not is_red(n.right), f"property 4: red-red at {n.key}"
        if left_leaning:
            assert not is_red(n.right), f"LLRB: right-leaning red at {n.key}"
        bl = walk(n.left, lo, n.key)
        br = walk(n.right, n.key, hi)
        assert bl == br, f"property 5: black-heights {bl} != {br} under {n.key}"
        assert n.size == 1 + size(n.left) + size(n.right), f"size field stale at {n.key}"
        return bl + (0 if is_red(n) else 1)
    return walk(root, None, None)

Pair it with the shortest correct insert there is, the LLRB version, which keeps exactly the properties the checker tests (with left_leaning=True):

def rotate_left(h):
    x = h.right
    h.right, x.left = x.left, h
    x.color, h.color = h.color, RED
    x.size = h.size
    h.size = 1 + size(h.left) + size(h.right)
    return x

def rotate_right(h):
    x = h.left
    h.left, x.right = x.right, h
    x.color, h.color = h.color, RED
    x.size = h.size
    h.size = 1 + size(h.left) + size(h.right)
    return x

def flip_colors(h):                     # split a temporary 4-node
    h.color = RED
    h.left.color = h.right.color = BLACK

def insert(h, key):
    if h is None:
        return Node(key, RED)
    if key < h.key:
        h.left = insert(h.left, key)
    elif key > h.key:
        h.right = insert(h.right, key)
    if is_red(h.right) and not is_red(h.left):
        h = rotate_left(h)
    if is_red(h.left) and is_red(h.left.left):
        h = rotate_right(h)
    if is_red(h.left) and is_red(h.right):
        flip_colors(h)
    h.size = 1 + size(h.left) + size(h.right)
    return h

def put(root, key):
    root = insert(root, key)
    root.color = BLACK                  # property 2, restored once per insert
    return root

import random
root, keys = None, set()
for _ in range(5000):
    k = random.randrange(100000)
    root = put(root, k); keys.add(k)
    bh = check(root, left_leaning=True)
assert size(root) == len(keys)
print("ok, black-height", bh)

Worked example: insert 10, 20, 30 into an empty LLRB. 10 becomes a black root. 20 goes right as red, which leans right, so a left rotation makes 20 the root with red 10 on its left. 30 goes right of 20 as red; now both children of 20 are red, a temporary 4-node, and the colour flip turns 10 and 30 black and 20 red, after which put blackens the root. Result: black 20 over black 10 and black 30, black-height 2 on every path, exactly the 2-3 tree you get by splitting the node 10|20|30.

Augmented fields and where these trees live

Real systems hang extra data on the nodes: subtree sizes for rank queries (an order-statistic tree), maximum endpoints for interval trees, sums for range queries. The properties say nothing about these fields, so an implementation can pass every colour test and still return wrong ranks. The rule that keeps augmentation correct is simple: a field that depends only on a node and its children survives recolouring untouched, must be recomputed for the two nodes involved in each rotation (lower node first, as in the code above), and must be recomputed along the search path after an insert or delete. Because rotations are O(1) and the path is O(log n), augmentation never changes the asymptotic cost. The checker's size assertion is the cheap guard that catches a forgotten update.

Where you meet these trees in practice: Java's TreeMap is a red-black tree, and since Java 8 a HashMap bin that grows past eight entries (TREEIFY_THRESHOLD) is converted to a red-black tree once the table has at least 64 buckets, which bounds the damage of many colliding keys. The C++ standard does not mandate red-black trees for std::map, but the major library implementations, libstdc++ among them, use one. Compare the alternatives in treaps (balance by random priorities) and skip lists (balance by coin flips, easier to make concurrent), and see LSM trees versus B-trees for why on-disk indexes use wide B-tree nodes rather than binary ones.

Failure modes

Failure modes worth testing for explicitly:

• Forgetting the root. The colour flip can turn the root red. The tree still has the right shape, but the next insert's case analysis assumes a black root. Blacken it after every operation.
• Null as a node. Code that reads node.color on a missing child crashes or, worse, treats NIL as red. Route every colour test through one is_red helper.
• Deletion fix-up with the wrong sibling. Most published bugs live in delete, where the sibling changes after a rotation. Randomised delete tests with the checker after every step find these in seconds.
• Duplicate keys. The checker above asserts strict ordering. If your map allows duplicates, pick a tie-breaking rule and test it, or store a count per node.
• Comparator inconsistency. A comparator that is not a total order silently breaks BST order; the checker's bounds test is the only thing that notices.
• Concurrent mutation. Rebalancing touches nodes far from the key being changed, so fine-grained locking is hard. Use a lock around the whole tree, a persistent version with path copying, or a skip list.

What to do next

1. Write the five properties from memory, then mark which two carry the height bound and why each alone fails.
2. Prove n is at least 2^h/2 - 1 on paper, then compute the height cap for your largest in-memory map.
3. Type in the checker and the LLRB insert above and run the randomised test; then break one line on purpose and confirm the checker names the property.
4. Draw a ten-key red-black tree as a 2-3-4 tree, and replay one insert as a B-tree split.
5. Add a rank query using the size field, and an assertion that ranks match a sorted list.
6. Work through deletion in the full walkthrough with the checker running after every step.