Chapter 18 - B-Trees

Chapter 18 starts with a first-pass mathematical B-tree model. Its specification-level search operation remains a compatibility oracle defined from membership, while searchExec is the separator-guided executable algorithm. On sorted, child-bounded trees, searchExec_true_iff is the semantic truth source connecting that algorithm to membership; searchExec_sound and searchExec_complete expose the two directions separately. findChild_localizes_mem proves that, in a sorted, child-bounded node, a non-separator member lies in the selected child. This localization result is used by the exact semantics proof for executable deletion, together with direct selected-child and predecessor-routing wrappers.

The current Lean surface additionally fixes direct base-search success/failure wrappers, the CLRS minimum-key height expression, base/positivity facts, height-step recurrence, height monotonicity, and specification-level split/insert/delete wrappers with split membership/search preservation plus direct split old-key corollaries, direct split validity, successful and unsuccessful search-after-update specifications, membership-driven search-after-update wrappers, and direct inserted/deleted-key plus old-key query preservation corollaries, direct validity short-name wrappers, equality-key update-query wrappers, Prop-level deletion success specifications, old failed-search preservation wrappers, together with exact failed membership specifications and direct failed-membership preservation wrappers after split, insert, and delete.

Section 18.1 now also connects the structural invariants to the textbook height analysis. totalKeys counts represented key slots without a uniqueness premise; the root lower bound explicitly separates the legal empty tree, while for 2 ≤ t, wellFormed_height_log_bound applies to every WellFormed tree and packages the CLRS logarithmic-height theorem.

Section 18.2 retains the flat insert as its specification layer and now proves the real top-level CLRS insertion operation insertRoot. splitRoot installs a full old root below a transient empty parent and applies the full-child split; the transient parent itself is not claimed WellFormed, but the split output is. Top-level insertion adds exactly one key, preserves WellFormed, has an exact same-or-one-higher conditional height theorem, agrees with the specification on membership and membership-oracle search, and supports correct executable search. This is an extensional compatibility result, not executable/specification tree-shape equality. Preservation of WellFormedUnique additionally requires that the inserted key was absent.

Section 18.3 also contains the executable node-level deletion proof. A single bundled induction proves key containment and the complete structural invariant packet across leaf deletion, separator replacement, rotations, and merges. Raw root deletion may produce an empty root with one child; the public composedDeleteRoot operation contracts that transient before exposing root-level well-formedness. Its key multiset is the input multiset after Multiset.erase removes one requested-key occurrence when present, assuming only the structural invariant and 2 ≤ t; membership of every different key is therefore preserved without uniqueness. Under WellFormedUnique, deletion also removes the requested key completely and agrees with the specification-level delete operation on membership and compatibility-oracle search. This is a semantic refinement, not a claim that the two operations return the same tree shape.

Sections

• 18.1 B-tree model, search, and height bound: proved for the current functional correctness model. Main results: CLRS.Chapter18.BTree.search_correct, CLRS.Chapter18.BTree.search_true_iff, CLRS.Chapter18.BTree.search_true_of_mem, CLRS.Chapter18.BTree.mem_of_search_true, CLRS.Chapter18.BTree.search_false_iff, CLRS.Chapter18.BTree.search_false_of_not_mem, CLRS.Chapter18.BTree.not_mem_of_search_false, CLRS.Chapter18.BTree.findChild, CLRS.Chapter18.BTree.findChild_localizes_mem, CLRS.Chapter18.BTree.searchExec, CLRS.Chapter18.BTree.searchExec_sound, CLRS.Chapter18.BTree.searchExec_complete, CLRS.Chapter18.BTree.searchExec_true_iff, CLRS.Chapter18.BTree.searchExec_eq_search, CLRS.Chapter18.BTree.minKeys_zero, CLRS.Chapter18.BTree.minKeys_pos, CLRS.Chapter18.BTree.one_le_minKeys, CLRS.Chapter18.BTree.minKeys_lower_bound, CLRS.Chapter18.BTree.minKeys_succ, CLRS.Chapter18.BTree.minKeys_le_succ, CLRS.Chapter18.BTree.minKeys_monotone_height, CLRS.Chapter18.BTree.totalKeys, CLRS.Chapter18.BTree.totalKeys_node, CLRS.Chapter18.BTree.nonRoot_totalKeys_add_one_lower_bound, CLRS.Chapter18.BTree.wellFormed_empty_or_totalKeys_add_one_lower_bound, CLRS.Chapter18.BTree.wellFormed_empty_or_minKeys_le_totalKeys, CLRS.Chapter18.BTree.wellFormed_minKeys_le_totalKeys, and CLRS.Chapter18.BTree.wellFormed_height_log_bound.

• 18.2 B-tree insertion: proved for the current functional correctness model. Main results: CLRS.Chapter18.BTree.splitChild_preserves_model, CLRS.Chapter18.BTree.splitChild_valid, CLRS.Chapter18.BTree.splitChild_mem_iff, CLRS.Chapter18.BTree.splitChild_mem_old, CLRS.Chapter18.BTree.splitChild_not_mem_iff, CLRS.Chapter18.BTree.splitChild_not_mem_old, CLRS.Chapter18.BTree.splitChild_search_iff, CLRS.Chapter18.BTree.splitChild_search_old, CLRS.Chapter18.BTree.splitChild_search_of_mem, CLRS.Chapter18.BTree.splitChild_search_false_iff, CLRS.Chapter18.BTree.splitChild_search_false_old, CLRS.Chapter18.BTree.splitChild_search_false_of_not_mem, CLRS.Chapter18.BTree.insert_preserves_model, CLRS.Chapter18.BTree.insert_valid, CLRS.Chapter18.BTree.insert_mem_iff, CLRS.Chapter18.BTree.insert_search_iff, CLRS.Chapter18.BTree.insert_mem_self, CLRS.Chapter18.BTree.insert_search_self, CLRS.Chapter18.BTree.insert_search_of_eq, CLRS.Chapter18.BTree.insert_mem_old, CLRS.Chapter18.BTree.insert_search_old, CLRS.Chapter18.BTree.insert_search_of_mem, CLRS.Chapter18.BTree.insert_not_mem_iff, CLRS.Chapter18.BTree.insert_not_mem_of_ne, CLRS.Chapter18.BTree.insert_search_false_iff, CLRS.Chapter18.BTree.insert_search_false_of_ne, CLRS.Chapter18.BTree.insert_search_false_of_not_mem_ne, CLRS.Chapter18.BTree.splitRoot, CLRS.Chapter18.BTree.insertRoot, CLRS.Chapter18.BTree.splitRoot_keys_perm, CLRS.Chapter18.BTree.splitRoot_wellFormed, CLRS.Chapter18.BTree.splitRoot_height, CLRS.Chapter18.BTree.splitRoot_rootKeyCount, CLRS.Chapter18.BTree.splitRoot_nonFull, CLRS.Chapter18.BTree.insertRoot_keys_perm, CLRS.Chapter18.BTree.insertRoot_wellFormed, CLRS.Chapter18.BTree.insertRoot_height, CLRS.Chapter18.BTree.insertRoot_mem_iff, CLRS.Chapter18.BTree.insertRoot_wellFormedUnique, CLRS.Chapter18.BTree.insertRoot_mem_iff_insert, CLRS.Chapter18.BTree.insertRoot_search_eq_insert, CLRS.Chapter18.BTree.insertRoot_searchExec_true_iff, and CLRS.Chapter18.BTree.insertRoot_correct.

• 18.3 B-tree deletion: proved for the current functional model. Main results: CLRS.Chapter18.BTree.delete_preserves_model, CLRS.Chapter18.BTree.delete_valid, CLRS.Chapter18.BTree.delete_mem_iff, CLRS.Chapter18.BTree.delete_mem_iff_ne, CLRS.Chapter18.BTree.delete_search_iff, CLRS.Chapter18.BTree.delete_search_iff_ne, CLRS.Chapter18.BTree.delete_not_mem, CLRS.Chapter18.BTree.delete_search_deleted_false, CLRS.Chapter18.BTree.delete_search_false_of_eq, CLRS.Chapter18.BTree.delete_mem_of_ne, CLRS.Chapter18.BTree.delete_mem_of_ne_prop, CLRS.Chapter18.BTree.delete_search_of_ne, CLRS.Chapter18.BTree.delete_search_of_ne_prop, CLRS.Chapter18.BTree.delete_search_of_mem_ne, CLRS.Chapter18.BTree.delete_search_of_mem_ne_prop, CLRS.Chapter18.BTree.delete_not_mem_iff, CLRS.Chapter18.BTree.delete_not_mem_old, CLRS.Chapter18.BTree.delete_not_mem_of_eq, CLRS.Chapter18.BTree.delete_search_false_iff, CLRS.Chapter18.BTree.delete_search_false_old, CLRS.Chapter18.BTree.delete_search_false_of_not_mem, CLRS.Chapter18.BTree.composedDelete_packet, CLRS.Chapter18.BTree.composedDelete_nonRoot_preserves, CLRS.Chapter18.BTree.composedDelete_rootResult, CLRS.Chapter18.BTree.keysOf_composedDelete_subset, CLRS.Chapter18.BTree.composedDelete_key_bound_lo, CLRS.Chapter18.BTree.composedDelete_key_bound_hi, CLRS.Chapter18.BTree.composedDelete_sameDepth_height, CLRS.Chapter18.BTree.composedDelete_sorted, CLRS.Chapter18.BTree.composedDelete_childBounded, CLRS.Chapter18.BTree.composedDelete_occupancy, CLRS.Chapter18.BTree.normalizeRoot_wellFormed, CLRS.Chapter18.BTree.composedDeleteRoot_keys_subset, CLRS.Chapter18.BTree.composedDeleteRoot_height, CLRS.Chapter18.BTree.composedDeleteRoot_wellFormed, CLRS.Chapter18.BTree.UniqueKeys, CLRS.Chapter18.BTree.WellFormedUnique, CLRS.Chapter18.BTree.findChild_pos_and_pred_eq_of_mem, CLRS.Chapter18.BTree.findChild_not_mem_child_of_ne, CLRS.Chapter18.BTree.findChild_selected_child_mem, CLRS.Chapter18.BTree.keyBag, CLRS.Chapter18.BTree.keyBag_erase_of_balance, CLRS.Chapter18.BTree.sortedRemove_keyBag, CLRS.Chapter18.BTree.mergeNodes_keyBag, CLRS.Chapter18.BTree.rotateRight_keyBag, CLRS.Chapter18.BTree.rotateLeft_keyBag, CLRS.Chapter18.BTree.replaceChild_keyBag_erase, CLRS.Chapter18.BTree.replacePredecessor_keyBag_erase, CLRS.Chapter18.BTree.replaceSuccessor_keyBag_erase, CLRS.Chapter18.BTree.spliceMerged_keyBag_erase, CLRS.Chapter18.BTree.rotateRight_reassembly_keyBag_erase, CLRS.Chapter18.BTree.rotateLeft_reassembly_keyBag_erase, CLRS.Chapter18.BTree.composedDelete_keyBag, CLRS.Chapter18.BTree.composedDelete_mem_iff_of_ne, CLRS.Chapter18.BTree.composedDelete_uniqueKeys, CLRS.Chapter18.BTree.composedDeleteRoot_keyBag, CLRS.Chapter18.BTree.composedDeleteRoot_mem_iff_of_ne, CLRS.Chapter18.BTree.composedDeleteRoot_not_mem, CLRS.Chapter18.BTree.composedDeleteRoot_mem_iff, CLRS.Chapter18.BTree.composedDeleteRoot_wellFormedUnique, CLRS.Chapter18.BTree.composedDeleteRoot_mem_iff_delete, CLRS.Chapter18.BTree.composedDeleteRoot_search_eq_delete, and CLRS.Chapter18.BTree.composedDeleteRoot_correct.

Completion Boundary

Search, top-level insertion and structural preservation, exact Multiset.erase deletion semantics, the structural total-key and logarithmic-height bounds, and the running-time / cost layer are complete under the documented assumptions for the current functional B-tree model. searchCost, insertCost, insertRootCost, and deleteCost mirror the executable searchExec, insertNonFull, insertRoot, and composedDelete constructions, and every one is bounded by heightOf + O(1); composing with wellFormed_height_log_bound gives the CLRS O(log_t n) disk-access bound (diskAccessBound). Disk-page layout, pointer mutation, and RAM semantics remain optional lower-level refinements.