Chapter 15 - Dynamic Programming

Chapter 15 studies optimal substructure and overlapping subproblems. The first CLRS-Lean pass covers four dynamic-programming examples at the mathematical optimality-interface level: rod cutting, matrix-chain multiplication, LCS, and optimal binary search trees. For rod cutting and OBST, the chapter records both the Bellman recurrence layer and an executable recurrence-valued function. For matrix-chain multiplication and LCS, the chapter records table/reconstruction certificates, recurrence wrappers on certified LCS tables, direct recurrence consequences for matching and nonmatching LCS heads, and pure recurrence and reconstruction functions. Except for rod cutting's array refinement, these are not yet the tabulated CLRS algorithms or their textbook cost models.

Sections

• 15.1 Rod cutting: partial. Main results: CLRS.Chapter15.firstCutValue_le_of_rodCutRecurrence, CLRS.Chapter15.bottomUpRodRevenue_rodCutRecurrence, CLRS.Chapter15.firstCutValue_le_of_rodCutTableRecurrence, CLRS.Chapter15.planValue_le_table_of_rodCutTableRecurrence, CLRS.Chapter15.planValue_le_bottomUpRodRevenue, CLRS.Chapter15.rodRevenue_le_of_firstCutValue_bounds, CLRS.Chapter15.planValue_le_revenue_of_rodCutRecurrence, CLRS.Chapter15.planValue_le_optimalPlanValue_of_same_length, CLRS.Chapter15.rodRevenueArray_correct, CLRS.Chapter15.rodRevenueArray_rodCutTableRecurrence, and CLRS.Chapter15.planValue_le_rodRevenueArray.

• 15.2 Matrix-chain multiplication: partial. Main results: CLRS.Chapter15.matrixChain_opt_le_planCost, CLRS.Chapter15.matrixChain_reconstructed_cost_eq, CLRS.Chapter15.matrixChain_reconstructed_optimal, CLRS.Chapter15.matrixChain_reconstructed_cost_le_planCost, CLRS.Chapter15.matrixChain_reconstructed_cost_eq_of_reconstructed, CLRS.Chapter15.matrixChainSplit_optimal, CLRS.Chapter15.matrixChainReconstruct_reconstructed, and CLRS.Chapter15.matrixChain_correct.

• 15.4 Longest common subsequence: partial. Main results: CLRS.Chapter15.LCSCertificate.commonSubsequence_length_le, CLRS.Chapter15.LCSCertificate.length_eq_of_certificates, and CLRS.Chapter15.isCommonSubsequence_comm, plus CLRS.Chapter15.LCSTableRecurrence.cons_cons, CLRS.Chapter15.LCSTableCertificate.nil_left, CLRS.Chapter15.LCSTableCertificate.nil_right, CLRS.Chapter15.LCSTableCertificate.cons_cons, CLRS.Chapter15.LCSTableCertificate.cons_cons_self, CLRS.Chapter15.LCSTableCertificate.cons_cons_of_eq, CLRS.Chapter15.LCSTableCertificate.diagonal_lt_cons_cons_of_eq, CLRS.Chapter15.LCSTableCertificate.cons_cons_of_ne, CLRS.Chapter15.LCSTableCertificate.drop_left_le_of_ne, CLRS.Chapter15.LCSTableCertificate.drop_right_le_of_ne, CLRS.Chapter15.LCSTableCertificate.commonSubsequence_length_le, CLRS.Chapter15.lcsTable_reconstruction_optimal, CLRS.Chapter15.lcsCertificate_of_table_reconstruction_length, and CLRS.Chapter15.lcs_correct.

• 15.5 Optimal binary search trees: partial. Main results: CLRS.Chapter15.OBST.obst_opt_le_planCost, CLRS.Chapter15.OBST.obst_reconstructed_cost_eq, CLRS.Chapter15.OBST.obst_reconstructed_optimal, CLRS.Chapter15.OBST.bottomUpOBST_obstRecurrence, and CLRS.Chapter15.OBST.obst_correct.

Current Gaps

The current files prove mathematical optimality interfaces for rod cutting, matrix-chain multiplication, LCS, and optimal binary search trees. Rod cutting and OBST have executable recurrence-valued functions, while matrix chain and LCS expose proved pure reconstruction procedures. OBST's public result is an existential optimal-plan theorem backed by a private witness construction. Rod cutting additionally has a mutable-Array bottom-up table (CLRS.Chapter15.rodRevenueArray) with a refinement theorem to the pure recurrence value. The other examples use pure recurrence evaluators or reconstruction certificates rather than proved CLRS-style tabulated implementations. Missing central layers include generic optimal-substructure/memoization interfaces, top-down cache correctness, matrix-chain/LCS/OBST table algorithms, and their textbook cost bounds.