Chapter 13 — Red-Black Trees

Native fourth-edition chapter guide.

Current source

This guide sources fourth-edition §13.1–§13.4 from the native section modules under CLRSLean.FourthEdition.Chapter_13. Declarations retain the CLRS.Chapter13 namespace; the legacy import CLRSLean.Chapter_13 and its Section_13_1_Red_Black_Trees module forward to these sources during the compatibility period.

Coverage boundary

The native color/black-height invariant layer and logarithmic-height theorem (§13.1), and the three fourth-edition section layers completing the §13.2–§13.4 boundaries:

• §13.1 (Section_13_1_Red_Black_Trees): the color and black-height invariants, membership preservation under rotations, the no-red-red property, the height_log_bound theorem (CLRS Lemma 13.1), and the functional insertion/deletion key-set and shape layers.

• §13.2 (Section_13_2_Rotations): a pointer/sentinel red-black store RBStore with representation predicate StoreRepr, pointer-level rotation/recolor primitives with constant cost, and BST/inorder preservation of rotations.

• §13.3 (Section_13_3_Insertion): the RB-INSERT-FIXUP inorder bridge (keys_balanceLeft/keys_balanceRight), BST output preservation bst_insert, and the logarithmic execution-cost theorem insertCost_log_bound.

• §13.4 (Section_13_4_Deletion): the logarithmic execution-cost theorem deleteCost_log_bound and BST ordering preservation of the composed delete bst_delete.

• The chapter-level WellFormed bundle combines RedBlackShape and BST; insert_correct and delete_correct preserve that invariant together with exact membership semantics.

Implementation details

The bundled client interface is available at Shape and BST correctness.

See docs/clrs-fourth-edition-map.csv for the section-level mapping and docs/migrations/clrs4.md for compatibility and deprecation policy.