Chapter 23 - Minimum Spanning Trees

Chapter 23 formalizes the mathematical correctness stack for minimum spanning trees: the cut property, canonical tree paths and exchange edges, end-to-end Kruskal optimality, and Prim optimality.

Sections

• 23.1 Growing a minimum spanning tree: main-proof-complete-for-correctness. Main results: CLRS.MST.Graph.connected_crosses_cut, CLRS.MST.FiniteGraph.minimumSpanningTree_of_mstExtending_empty, CLRS.MST.FiniteGraph.mstExtending_empty_of_minimumSpanningTree, CLRS.MST.FiniteGraph.minimumSpanningTree_iff_mstExtending_empty, CLRS.MST.FiniteGraph.exists_crossing_tree_edge_of_cut, CLRS.MST.FiniteGraph.exists_crossing_tree_edge_preserving_prefix, and CLRS.MST.safe_edge_of_lightest_crossing.

• 23.2 Kruskal and Prim: main-proof-complete-for-correctness. Closure results: CLRS.MST.FiniteGraph.canonicalSimplePath_unique, CLRS.MST.FiniteGraph.exists_crossing_exchangePath_of_spanningTree, CLRS.MST.FiniteGraph.cutCertificate_of_lightest_crossing_auto, CLRS.MST.FiniteGraph.kruskal_minimum_spanning_tree_of_sorted_complete_exact_component_empty, and CLRS.MST.FiniteGraph.prim_minimum_spanning_tree.

Current Shape

Section 23.1 supplies the reusable cut-property kernel and concrete finite-graph MST specification. Section 23.2 proves that a selected forest induces an acyclic simple graph with a unique canonical path. A path crossing a cut automatically yields the exchange edge and the two residual connections needed by ExchangePath, eliminating the former manual cycle certificate.

Kruskal's proof now carries the processed prefix through the recursion, derives local sorted lightness from exact components, constructs every exchange certificate internally, and discharges the final spanning-tree condition for a complete connected scan. Prim is represented by a dynamic light-edge trace; the shared cut property proves safe extension, exact components prove forest preservation, and a complete trace returns a concrete minimum spanning tree.

The implementation layer threads the actual costed union-find machine through Kruskal and proves connectivity/output refinement. Its combined work expression adds an independent sorting budget to the scan and union-find counters.

The canonical fourth-edition Chapter 21 imports completion proofs for the frontier run and a cached array Prim execution. The latter constructs its own MST and counts queue/index preparation, array reads/writes, key comparisons and adjacency visits, with a 2n² + 5n + 6E bound. The existing binary-heap formula is conditional on backend operations; it is not the cost of the reference frontier rescan or an implemented binary heap. The new array variant supplies its own concrete queue proof. Allocation and bit costs remain outside these abstract operation models.