CLRS-Lean
Chapter 15. Dynamic Programming

Imports

import CLRSLean.Chapter_15.Section_15_1_Rod_Cutting
import CLRSLean.Chapter_15.Section_15_2_Matrix_Chain_Multiplication
import CLRSLean.Chapter_15.Section_15_4_Longest_Common_Subsequence

Chapter 15 - Dynamic Programming

Chapter 15 studies optimal substructure and overlapping subproblems. The first CLRS-Lean pass covers three dynamic-programming examples at the mathematical optimality-interface level: rod cutting, matrix-chain multiplication, and LCS. For rod cutting, the chapter now records both the Bellman recurrence layer and a finite bottom-up table-certificate layer, plus 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 direct reconstruction optimality inequalities, while concrete mutable-array implementations remain future refinements.

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, and CLRS.Chapter15.planValue_le_optimalPlanValue_of_same_length.
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, and CLRS.Chapter15.matrixChain_reconstructed_cost_eq_of_reconstructed.
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, and CLRS.Chapter15.lcsCertificate_of_table_reconstruction_length.

Current Gaps

The current files prove mathematical optimality interfaces for rod cutting, matrix-chain multiplication, and LCS. Rod cutting now has a finite table-prefix correctness theorem and executable recurrence-valued function; mutable-array table construction, memoized recursion, executable reconstruction procedures, and optimal binary search trees are future section targets.

              namespace CLRSnamespace Chapter15end Chapter15end CLRS