Chapter 13 - Red-Black Trees

Chapter 13 proves that red-black trees maintain logarithmic height through color and black-height invariants. The current CLRS-Lean pass builds the local invariant layer: colored trees, membership preservation under rotations, the no-red-red property, black-height balance, root recoloring, and a bundled local red-black shape predicate. It also isolates the four local RB-INSERT-FIXUP rotation/recoloring cases as small certificates that preserve membership and local black height while establishing shape. These case certificates are also bundled through one local dispatcher interface.

Sections

• 13.1 Red-black trees: partial. Main results: CLRS.Chapter13.RBTree.inTree_rotateLeft_iff, CLRS.Chapter13.RBTree.inTree_rotateRight_iff, CLRS.Chapter13.RBTree.inTree_repaintRoot_iff, CLRS.Chapter13.RBTree.noRedRed_repaint_black, CLRS.Chapter13.RBTree.balancedBlackHeight_repaintRoot, CLRS.Chapter13.RBTree.balancedBlackHeight_rotateLeft_red_red, CLRS.Chapter13.RBTree.balancedBlackHeight_rotateRight_red_red, CLRS.Chapter13.RBTree.redBlackShape_repaint_rotateLeft_red_red, CLRS.Chapter13.RBTree.redBlackShape_repaint_rotateRight_red_red, CLRS.Chapter13.RBTree.redBlackShape_repaint_black, CLRS.Chapter13.RBTree.inTree_insertFixup_leftLeft_iff, CLRS.Chapter13.RBTree.inTree_insertFixup_leftRight_iff, CLRS.Chapter13.RBTree.inTree_insertFixup_rightLeft_iff, CLRS.Chapter13.RBTree.inTree_insertFixup_rightRight_iff, CLRS.Chapter13.RBTree.blackHeight_insertFixup_leftLeft, CLRS.Chapter13.RBTree.blackHeight_insertFixup_leftRight, CLRS.Chapter13.RBTree.blackHeight_insertFixup_rightLeft, CLRS.Chapter13.RBTree.blackHeight_insertFixup_rightRight, CLRS.Chapter13.RBTree.redBlackShape_insertFixup_leftLeft, CLRS.Chapter13.RBTree.redBlackShape_insertFixup_leftRight, CLRS.Chapter13.RBTree.redBlackShape_insertFixup_rightLeft, CLRS.Chapter13.RBTree.redBlackShape_insertFixup_rightRight, CLRS.Chapter13.RBTree.insertFixupLocal_leftLeft_certificate, CLRS.Chapter13.RBTree.insertFixupLocal_leftRight_certificate, CLRS.Chapter13.RBTree.insertFixupLocal_rightLeft_certificate, and CLRS.Chapter13.RBTree.insertFixupLocal_rightRight_certificate.

Current Gaps

The full CLRS insertion and deletion algorithms are not yet mechanized. The next insertion step is to compose the local fixup certificates into an executable RB-INSERT-FIXUP; deletion fixup and the logarithmic-height theorem remain larger future targets.