Ch14.3: toRB refinement erasure for the generic AugmentedRBTree deletion pipeline

[TankTechnology]

The remaining refinement gap in the generic augmentation story (CLRS §14.3).

Status

The generic executable insertion and deletion pipelines are proved, including for any augmentation. The remaining piece is the refinement erasure: proving that erasing the augmentation from the generic deletion pipeline (the ///// smart constructors) reproduces Chapter 13's , mirroring the refinement already proved for order-statistic trees in §14.1.

Scope

• (augmentation-erasing projection) commutes with each ///// step;
• the refinement erasure for the full generic deletion pipeline, giving -style theorems for ;
• keys/ correspondence through the deletion pipeline.

This is the Chapter-13 refinement erasure work flagged as "future work" in .

[TankTechnology]

Verified on main: the toRB refinement erasure for the deletion pipeline exists. CLRSLean/Chapter_14/Section_14_3_Interval_Trees.lean proves theorem toRB_delete (x : Nat) (t : AugmentedRBTree Nat β): erasing the augmentation commutes with recursive deletion, mirroring the toRB_insert refinement (§14.1). The generic deletion pipeline and its erasure are both present. Closing as covered.