Chapter 14 - Augmenting Data Structures

Chapter 14 explains how to attach auxiliary information to a data structure and maintain enough local consistency to support stronger queries. The first CLRS-Lean pass formalizes the mathematical core of order-statistic trees: each node stores a subtree size, and rank selection uses the left-subtree size to choose a branch. The rotation layer now exposes cached-root-size preservation, ideal rank-selection preservation, and the corresponding augmented-selector wrapper for well-sized trees. It also exposes a recompute-then-rotate bridge: from any tree, recomputing size fields before a local rotation produces a well-sized tree whose augmented selector still agrees with the original ideal rank selector.

Sections

• 14.1 Order-statistic trees: partial. Main results: CLRS.Chapter14.OSTree.storedSize_eq_realSize_of_wellSized, CLRS.Chapter14.OSTree.recomputeSizes_wellSized, CLRS.Chapter14.OSTree.keys_recomputeSizes, and CLRS.Chapter14.OSTree.keys_rotateLeft, CLRS.Chapter14.OSTree.keys_rotateRight, CLRS.Chapter14.OSTree.realSize_rotateLeft, CLRS.Chapter14.OSTree.realSize_rotateRight, CLRS.Chapter14.OSTree.storedSize_rotateLeft_of_wellSized, CLRS.Chapter14.OSTree.storedSize_rotateRight_of_wellSized, CLRS.Chapter14.OSTree.rankSelect?_rotateLeft, CLRS.Chapter14.OSTree.rankSelect?_rotateRight, CLRS.Chapter14.OSTree.rotateLeft_wellSized, CLRS.Chapter14.OSTree.rotateRight_wellSized, and CLRS.Chapter14.OSTree.osSelect?_eq_rankSelect?_of_wellSized, CLRS.Chapter14.OSTree.osSelect?_rotateLeft_eq_rankSelect?_of_wellSized, CLRS.Chapter14.OSTree.osSelect?_rotateRight_eq_rankSelect?_of_wellSized, CLRS.Chapter14.OSTree.realSize_recomputeSizes, CLRS.Chapter14.OSTree.rankSelect?_recomputeSizes, CLRS.Chapter14.OSTree.rotateLeft_recomputeSizes_wellSized, CLRS.Chapter14.OSTree.rotateRight_recomputeSizes_wellSized, CLRS.Chapter14.OSTree.osSelect?_rotateLeft_recomputeSizes_eq_rankSelect?, and CLRS.Chapter14.OSTree.osSelect?_rotateRight_recomputeSizes_eq_rankSelect?.

Current Gaps

The current model proves the augmentation invariant and rank-selection correctness for a functional tree, including size-preserving local rotations. The recompute-then-rotate bridge is ready to be used by a future red-black balancing refinement. The model does not yet connect those rotations to full Chapter 13 insertion/deletion fixup, interval trees, or the general augmentation theorem from the textbook.