Derivation — Insertion and Deletion in Red-Black Trees

The previous lesson stated the red-black properties and claimed that rotations restore them cheaply after any mutation, without showing the mechanism. This derivation works through the case analysis for insertion fix-up in full (deletion fix-up is structurally similar but longer; it is summarised at the level CLRS itself uses for a second pass) and shows why the case analysis terminates in $O(\log n)$ rotations — in fact at most $O(1)$ actual rotations, with $O(\log n)$ colour flips.