Chapter 18 - B-Trees

Chapter 18 starts with a first-pass mathematical B-tree model. The current Lean surface fixes key membership, search correctness, 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.

Sections

• 18.1 B-tree model: partial. 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.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, and CLRS.Chapter18.BTree.minKeys_monotone_height.

• 18.2 B-tree insertion: partial. 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, and CLRS.Chapter18.BTree.insert_search_false_of_not_mem_ne.

• 18.3 B-tree deletion: partial. 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, and CLRS.Chapter18.BTree.delete_search_false_of_not_mem.

Current Gaps

Full node occupancy, separator ordering, same-depth leaves, in-node splitting, node-level deletion repair, and disk-page semantics remain strengthening targets.