Section 24.5 is the only unrepresented section in Chapter 24 (24.1-24.4 are proved). It formalizes the algebraic properties of shortest paths that CLRS proves in prose: subpath property, triangle inequality on distances, optimal substructure, and convergence/successor relaxation lemmas.
Scope
A compact lemma file proving the distance/subpath identities for the existing shortest-path model, likely reusable by the Bellman-Ford/DAG/Dijkstra correctness proofs in 24.1-24.3. Low difficulty; moderate value.
Section 24.5 is the only unrepresented section in Chapter 24 (24.1-24.4 are proved). It formalizes the algebraic properties of shortest paths that CLRS proves in prose: subpath property, triangle inequality on distances, optimal substructure, and convergence/successor relaxation lemmas.
Scope
A compact lemma file proving the distance/subpath identities for the existing shortest-path model, likely reusable by the Bellman-Ford/DAG/Dijkstra correctness proofs in 24.1-24.3. Low difficulty; moderate value.