Kruskal's Minimum Spanning Forest and Tree Algorithm

This module formalizes Kruskal's greedy algorithm for minimum-weight spanning forests and minimum spanning trees on finite multigraphs over Fin n, together with its functional correctness, global optimality, distinct-weight uniqueness, Cslib.DataStructure disjoint-set client specification, and TimeM comparison and disjoint-set step bounds.

Mathematical model and source mapping

An input multigraph on n vertices is represented as a finite list es : List (WeightedEdge n W) of undirected weighted edges (u, v, weight) with u v : Fin n (allowing parallel edges, self-loops, disconnected graphs, and negative or duplicate weights). Connectivity is tracked via Cslib.DataStructure.DisjointSet.Partition n:

• edgePartitionFrom p es folds Partition.merge across es starting from p, and edgePartition es := edgePartitionFrom (Partition.discrete n) es is the induced connected-component partition on Fin n.
• IsAcyclic F states the exact component-edge conservation law (edgePartition F).numComponents + F.length = n: starting from n isolated vertices, every edge in F merges two previously distinct connected components. The companion module CslibFrontier.Algorithms.Lean.Kruskal.SimpleGraph bridges IsAcyclic, IsSpanningForest, and IsSpanningTree to Mathlib's SimpleGraph.IsAcyclic, maximal acyclic subgraphs, and SimpleGraph.IsTree.
• IsSpanningForest es F requires F.Subperm es, IsAcyclic F, and edgePartition F = edgePartition es (matching maximal forest subgraphs of es).

Primary-source correspondence:

• Cormen et al., Chapter 23, Section 23.1 (Theorem 23.1, pp. 626–628, and Corollary 23.2, p. 628) and Section 23.2 (MST-KRUSKAL, pp. 631–633): [CLRS2009] formulates Theorem 23.1 and MST-KRUSKAL for connected, simple undirected graphs with real-valued edge weights. Here kruskalEdges sorts es in nondecreasing weight order via List.mergeSort and scans the sorted list, accepting each edge whose endpoints lie in distinct components; kruskalEdges_isMinSpanningForest generalizes global weight optimality to arbitrary finite multigraphs (connected or disconnected, with parallel edges, self-loops, and negative or equal weights) over any [AddCommMonoid W] [LinearOrder W] [IsOrderedAddMonoid W], and kruskalEdges_isMinSpanningTree specializes to connected inputs ((edgePartition es).numComponents = 1).
• Kruskal, Opening paragraph, Construction A, and uniqueness proof, pp. 48–50: Kruskal's original paper assumes a finite connected graph with distinct positive real edge lengths and proves (T = A_{n-1}, p. 50) that Construction A yields the unique shortest spanning subtree. Here perm_kruskalEdges_of_isMinSpanningForest_of_nodup_weights generalizes uniqueness (up to list permutation, hence exact edge-multiset equality) to arbitrary finite multigraphs (connected or disconnected) with distinct weights in any [AddCancelCommMonoid W] [LinearOrder W] [IsOrderedCancelAddMonoid W].

Cost model and limitations

kruskalM executes Kruskal's algorithm in TimeM Cost with two separate operation counters:

• Cost.comparisons: exact number of edge-weight comparisons decide (a.weight ≤ b.weight) performed by List.mergeSortM, bounded by m * Nat.clog 2 m (m = es.length) via Cslib.Algorithms.Lean.TimeM.time_mergeSortM_le.
• Cost.ufSteps: exact number of disjoint-set forest steps (find parent-pointer inspections plus union root links) recorded by Cslib.DataStructure.DisjointSet.UnionFind.run on kruskalClient, bounded by m * (2 * Nat.log 2 n + 3) via DisjointSet.UnionFind.run_correct (worst-case O(log n) per operation from union by rank, rather than Tarjan's amortized O(α(n)) inverse-Ackermann bound).
• realized_kruskal additionally decouples Kruskal's scan from any particular concrete forest: for any Cslib.DataStructure.StateTransitionImpl and Cslib.DataStructure.Bound for DisjointSet.spec n there is an execution of kruskalClient (sortEdges es) whose total cost is at most the certificate's total charge.

DisjointSet.UnionFind.init n (O(n) MAKE-SET initialization in [CLRS2009], MST-KRUSKAL lines 2–3, pp. 631, 633), list splitting/allocation in List.mergeSortM and kruskalClient, and pure Lean array updates inside Batteries.UnionFind carry 0 TimeM Cost charge (so Cost records only sorting weight comparisons and post-initialization UnionFind find/union steps, not Word-RAM instructions; if a Batteries.UnionFind value were shared non-linearly, array updates could copy, whereas DisjointSet.UnionFind.run threads its state single-threadedly).

Main definitions

• WeightedEdge, totalWeight: weighted undirected multigraph edges on Fin n and edge-list weight sum.
• edgePartitionFrom, edgePartition: connected-component partitions induced by an edge list.
• IsAcyclicFrom, IsAcyclic, IsSpanningForest, IsSpanningTree, IsMinSpanningForest, IsMinSpanningTree: forest, spanning-forest, spanning-tree, and minimum-weight predicates.
• kruskalScan, sortEdges, kruskalEdges: pure Kruskal scan, weight merge-sort, and Kruskal's algorithm.
• kruskalClient: DisjointSet.spec n client for the Kruskal cycle-filtering pass.
• Cost, Output, sortEdgesM, kruskalScanM, kruskalM: structured two-resource cost profile, algorithm output, and TimeM implementations.

Main results

• rel_edgePartitionFrom_iff_eqvGen, rel_edgePartition_iff_eqvGen: exact Relation.EqvGen characterization of edge-induced partitions.
• numComponents_le_edgePartitionFrom_add_length, isAcyclicFrom_cons: component-count lower bound and inductive characterization of relative acyclicity.
• kruskalEdges_isSpanningForest, kruskalEdges_isMinSpanningForest, kruskalEdges_isMinSpanningTree: Kruskal's algorithm computes a minimum-weight spanning forest (and a minimum spanning tree when connected).
• perm_kruskalEdges_of_isMinSpanningForest_of_nodup_weights: uniqueness of the minimum spanning forest up to permutation when edge weights are pairwise distinct.
• realized_kruskal: for any realization of DisjointSet.spec n with a resource bound, existence of a Cslib.DataStructure execution of the Kruskal client that returns kruskalEdges es within that bound.
• kruskalM_forest, kruskalM_rep, kruskalM_comparisons_le, kruskalM_ufSteps_le, kruskalM_total_le: functional correctness, final union-find representation, m ⌈log₂ m⌉ comparison bound, and m (2 ⌊log₂ n⌋ + 3) disjoint-set step bound for kruskalM.

References

• J. B. Kruskal, Jr., On the Shortest Spanning Subtree of a Graph and the Traveling Salesman Problem
• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Chapter 23

Weighted edges and edge-induced partitions

structure Cslib.Algorithms.Lean.Kruskal.WeightedEdge (n : ℕ) (W : Type) : Type

A weighted undirected edge on Fin n (allowing parallel edges and self-loops).

• u : Fin n

  First endpoint.

• v : Fin n

  Second endpoint.

• weight : W

  Edge weight.

def Cslib.Algorithms.Lean.Kruskal.instReprWeightedEdge.repr {n✝ : ℕ} {W✝ : Type} [Repr W✝] : WeightedEdge n✝ W✝ → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Algorithms.Lean.Kruskal.instReprWeightedEdge {n✝ : ℕ} {W✝ : Type} [Repr W✝] : Repr (WeightedEdge n✝ W✝)

@[instance_reducible]

instance Cslib.Algorithms.Lean.Kruskal.WeightedEdge.instDecidableEq {n : ℕ} {W : Type} [DecidableEq W] : DecidableEq (WeightedEdge n W)

def Cslib.Algorithms.Lean.Kruskal.WeightedEdge.endpoints {n : ℕ} {W : Type} (e : WeightedEdge n W) : Fin n × Fin n

Endpoint pair (e.u, e.v) forgetting the weight, for interoperability with unweighted DisjointSet.spanningForestEdges.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.WeightedEdge.endpoints_fst {n : ℕ} {W : Type} (e : WeightedEdge n W) : e.endpoints.1 = e.u

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.WeightedEdge.endpoints_snd {n : ℕ} {W : Type} (e : WeightedEdge n W) : e.endpoints.2 = e.v

def Cslib.Algorithms.Lean.Kruskal.totalWeight {n : ℕ} {W : Type} [AddCommMonoid W] (es : List (WeightedEdge n W)) : W

Total weight of an edge list.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.totalWeight_nil {n : ℕ} {W : Type} [AddCommMonoid W] : totalWeight [] = 0

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.totalWeight_cons {n : ℕ} {W : Type} [AddCommMonoid W] (e : WeightedEdge n W) (es : List (WeightedEdge n W)) : totalWeight (e :: es) = e.weight + totalWeight es

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.totalWeight_append {n : ℕ} {W : Type} [AddCommMonoid W] (es₁ es₂ : List (WeightedEdge n W)) : totalWeight (es₁ ++ es₂) = totalWeight es₁ + totalWeight es₂

theorem Cslib.Algorithms.Lean.Kruskal.Perm.totalWeight_eq {n : ℕ} {W : Type} [AddCommMonoid W] {es₁ es₂ : List (WeightedEdge n W)} (h : es₁.Perm es₂) : totalWeight es₁ = totalWeight es₂

Permuting an edge list preserves its total weight.

theorem Cslib.Algorithms.Lean.Kruskal.Sublist.totalWeight_le {n : ℕ} {W : Type} [AddCommMonoid W] [Preorder W] [IsOrderedAddMonoid W] {es₁ es₂ : List (WeightedEdge n W)} (h : es₁.Sublist es₂) (hnonneg : ∀ e ∈ es₂, 0 ≤ e.weight) : totalWeight es₁ ≤ totalWeight es₂

Deleting edges of nonnegative weight does not increase the total weight.

def Cslib.Algorithms.Lean.Kruskal.edgePartitionFrom {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (es : List (WeightedEdge n W)) : DataStructure.DisjointSet.Partition n

Partition obtained by merging the endpoints of every edge in es starting from p.

def Cslib.Algorithms.Lean.Kruskal.edgePartition {n : ℕ} {W : Type} (es : List (WeightedEdge n W)) : DataStructure.DisjointSet.Partition n

Connected-component partition of Fin n induced by es.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.edgePartitionFrom_nil {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) : edgePartitionFrom p [] = p

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.edgePartitionFrom_cons {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (e : WeightedEdge n W) (es : List (WeightedEdge n W)) : edgePartitionFrom p (e :: es) = edgePartitionFrom (p.merge e.u e.v) es

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.edgePartitionFrom_append {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (es₁ es₂ : List (WeightedEdge n W)) : edgePartitionFrom p (es₁ ++ es₂) = edgePartitionFrom (edgePartitionFrom p es₁) es₂

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.edgePartition_nil {n : ℕ} {W : Type} : edgePartition [] = DataStructure.DisjointSet.Partition.discrete n

theorem Cslib.Algorithms.Lean.Kruskal.edgePartitionFrom_eq_eval_spanningForestEdges {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (es : List (WeightedEdge n W)) : edgePartitionFrom p es = (DataStructure.eval (DataStructure.DisjointSet.spec n) (DataStructure.DisjointSet.spanningForestEdges WeightedEdge.endpoints es) p).2

edgePartitionFrom p es is the final partition reached by DisjointSet.spanningForestEdges WeightedEdge.endpoints es.

theorem Cslib.Algorithms.Lean.Kruskal.rel_edgePartitionFrom_iff_eqvGen {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (es : List (WeightedEdge n W)) (a b : Fin n) : (edgePartitionFrom p es).rel a b = true ↔ Relation.EqvGen (fun (x y : Fin n) => p.rel x y = true ∨ ∃ e ∈ es, x = e.u ∧ y = e.v) a b

Exact equivalence-closure characterization of edgePartitionFrom p es.

theorem Cslib.Algorithms.Lean.Kruskal.rel_edgePartition_iff_eqvGen {n : ℕ} {W : Type} (es : List (WeightedEdge n W)) (a b : Fin n) : (edgePartition es).rel a b = true ↔ Relation.EqvGen (fun (x y : Fin n) => ∃ e ∈ es, x = e.u ∧ y = e.v) a b

Two vertices are in the same component of edgePartition es iff they are connected by the equivalence closure of the edges in es.

theorem Cslib.Algorithms.Lean.Kruskal.rel_edgePartitionFrom_of_mem {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) {e : WeightedEdge n W} {es : List (WeightedEdge n W)} (he : e ∈ es) : (edgePartitionFrom p es).rel e.u e.v = true

Every edge in es relates its endpoints in edgePartitionFrom p es.

theorem Cslib.Algorithms.Lean.Kruskal.Perm.edgePartitionFrom_eq {n : ℕ} {W : Type} {es₁ es₂ : List (WeightedEdge n W)} (h : es₁.Perm es₂) (p : DataStructure.DisjointSet.Partition n) : edgePartitionFrom p es₁ = edgePartitionFrom p es₂

edgePartitionFrom is invariant under edge-list permutations.

theorem Cslib.Algorithms.Lean.Kruskal.Perm.edgePartition_eq {n : ℕ} {W : Type} {es₁ es₂ : List (WeightedEdge n W)} (h : es₁.Perm es₂) : edgePartition es₁ = edgePartition es₂

edgePartition is invariant under edge-list permutations.

theorem Cslib.Algorithms.Lean.Kruskal.edgePartitionFrom_merge {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (x y : Fin n) (es : List (WeightedEdge n W)) : edgePartitionFrom (p.merge x y) es = (edgePartitionFrom p es).merge x y

Merging (x, y) before folding es is equal to folding es and then merging (x, y).

theorem Cslib.Algorithms.Lean.Kruskal.numComponents_le_edgePartitionFrom_add_length {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (es : List (WeightedEdge n W)) : p.numComponents ≤ (edgePartitionFrom p es).numComponents + es.length

Each edge reduces the number of connected components by at most 1.

Relative acyclicity, spanning forests, and spanning trees

def Cslib.Algorithms.Lean.Kruskal.IsAcyclicFrom {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (F : List (WeightedEdge n W)) : Prop

F is acyclic relative to an initial partition p when every edge in F merges two distinct components, decreasing the component count by F.length.

def Cslib.Algorithms.Lean.Kruskal.IsAcyclic {n : ℕ} {W : Type} (F : List (WeightedEdge n W)) : Prop

An edge list F on Fin n is acyclic (a forest) when each edge merges two distinct connected components starting from Partition.discrete n, i.e., (edgePartition F).numComponents + F.length = n.

@[instance_reducible]

instance Cslib.Algorithms.Lean.Kruskal.instDecidableIsAcyclicFrom {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (F : List (WeightedEdge n W)) : Decidable (IsAcyclicFrom p F)

@[instance_reducible]

instance Cslib.Algorithms.Lean.Kruskal.instDecidableIsAcyclic {n : ℕ} {W : Type} (F : List (WeightedEdge n W)) : Decidable (IsAcyclic F)

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.isAcyclicFrom_nil {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) : IsAcyclicFrom p []

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.isAcyclic_nil {n : ℕ} {W : Type} : IsAcyclic []

theorem Cslib.Algorithms.Lean.Kruskal.isAcyclic_iff {n : ℕ} {W : Type} (F : List (WeightedEdge n W)) : IsAcyclic F ↔ (edgePartition F).numComponents + F.length = n

theorem Cslib.Algorithms.Lean.Kruskal.isAcyclicFrom_cons {n : ℕ} {W : Type} {p : DataStructure.DisjointSet.Partition n} {e : WeightedEdge n W} {F : List (WeightedEdge n W)} : IsAcyclicFrom p (e :: F) ↔ p.rel e.u e.v = false ∧ IsAcyclicFrom (p.merge e.u e.v) F

Inductive characterization of relative acyclicity: e :: F is acyclic over p iff e's endpoints lie in distinct classes of p and F is acyclic over p.merge e.u e.v.

theorem Cslib.Algorithms.Lean.Kruskal.Perm.isAcyclicFrom_iff {n : ℕ} {W : Type} {p : DataStructure.DisjointSet.Partition n} {F₁ F₂ : List (WeightedEdge n W)} (h : F₁.Perm F₂) : IsAcyclicFrom p F₁ ↔ IsAcyclicFrom p F₂

Relative acyclicity is invariant under edge-list permutations.

theorem Cslib.Algorithms.Lean.Kruskal.Perm.isAcyclic_iff {n : ℕ} {W : Type} {F₁ F₂ : List (WeightedEdge n W)} (h : F₁.Perm F₂) : IsAcyclic F₁ ↔ IsAcyclic F₂

Acyclicity is invariant under edge-list permutations.

theorem Cslib.Algorithms.Lean.Kruskal.IsAcyclic.length_le {n : ℕ} {W : Type} {F : List (WeightedEdge n W)} (hF : IsAcyclic F) : F.length ≤ n

Every acyclic edge list on Fin n has at most n edges (and at most n - 1 when 0 < n).

theorem Cslib.Algorithms.Lean.Kruskal.IsAcyclic.length_le_pred {n : ℕ} {W : Type} {F : List (WeightedEdge n W)} (hn : 0 < n) (hF : IsAcyclic F) : F.length + 1 ≤ n

theorem Cslib.Algorithms.Lean.Kruskal.IsAcyclic.ne_of_mem {n : ℕ} {W : Type} {F : List (WeightedEdge n W)} (hF : IsAcyclic F) {e : WeightedEdge n W} (he : e ∈ F) : e.u ≠ e.v

No self-loop belongs to an acyclic edge list.

def Cslib.Algorithms.Lean.Kruskal.IsSpanningForestFrom {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (es F : List (WeightedEdge n W)) : Prop

Relative spanning forest of es starting from partition p.

def Cslib.Algorithms.Lean.Kruskal.IsSpanningForest {n : ℕ} {W : Type} (es F : List (WeightedEdge n W)) : Prop

F is a spanning forest of the multigraph es when F is a sub-multiset (Subperm) of es, F is acyclic, and F induces the exact same connected components as es.

def Cslib.Algorithms.Lean.Kruskal.IsSpanningTree {n : ℕ} {W : Type} (es T : List (WeightedEdge n W)) : Prop

T is a spanning tree of es when T is a sub-multiset of es, T is acyclic, and T connects Fin n into a single component (numComponents = 1).

def Cslib.Algorithms.Lean.Kruskal.IsMinSpanningForest {n : ℕ} {W : Type} [AddCommMonoid W] [LE W] (es F : List (WeightedEdge n W)) : Prop

F is a minimum-weight spanning forest of es when F is a spanning forest of es of minimum totalWeight.

def Cslib.Algorithms.Lean.Kruskal.IsMinSpanningTree {n : ℕ} {W : Type} [AddCommMonoid W] [LE W] (es T : List (WeightedEdge n W)) : Prop

T is a minimum-weight spanning tree of es when T is a spanning tree of es of minimum totalWeight.

theorem Cslib.Algorithms.Lean.Kruskal.isSpanningForest_iff_from_discrete {n : ℕ} {W : Type} (es F : List (WeightedEdge n W)) : IsSpanningForest es F ↔ IsSpanningForestFrom (DataStructure.DisjointSet.Partition.discrete n) es F

theorem Cslib.Algorithms.Lean.Kruskal.isSpanningTree_iff_isSpanningForest_of_connected {n : ℕ} {W : Type} {es T : List (WeightedEdge n W)} (hconn : (edgePartition es).numComponents = 1) : IsSpanningTree es T ↔ IsSpanningForest es T

Every spanning tree on a connected multigraph (edgePartition es).numComponents = 1 is a spanning forest, and vice versa.

theorem Cslib.Algorithms.Lean.Kruskal.IsSpanningTree.length_add_one {n : ℕ} {W : Type} {es T : List (WeightedEdge n W)} (hT : IsSpanningTree es T) : T.length + 1 = n

Every spanning tree on Fin n has n - 1 edges (T.length + 1 = n).

theorem Cslib.Algorithms.Lean.Kruskal.IsSpanningForest.length_eq {n : ℕ} {W : Type} {es F₁ F₂ : List (WeightedEdge n W)} (h₁ : IsSpanningForest es F₁) (h₂ : IsSpanningForest es F₂) : F₁.length = F₂.length

All spanning forests of the same multigraph es have the exact same cardinality n - (edgePartition es).numComponents.

Pure Kruskal scan, merge-sort, optimality, and uniqueness

def Cslib.Algorithms.Lean.Kruskal.kruskalScan {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) : List (WeightedEdge n W) → List (WeightedEdge n W)

Greedy Kruskal scan starting from partition p: inspect edges in order, accepting an edge iff its endpoints currently lie in distinct classes of p.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.kruskalScan_nil {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) : kruskalScan p [] = []

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.kruskalScan_cons {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (e : WeightedEdge n W) (es : List (WeightedEdge n W)) : kruskalScan p (e :: es) = if (!p.rel e.u e.v) = true then e :: kruskalScan (p.merge e.u e.v) es else kruskalScan p es

theorem Cslib.Algorithms.Lean.Kruskal.kruskalScan_eq_eval_spanningForestEdges {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (es : List (WeightedEdge n W)) : kruskalScan p es = (DataStructure.eval (DataStructure.DisjointSet.spec n) (DataStructure.DisjointSet.spanningForestEdges WeightedEdge.endpoints es) p).1

kruskalScan p es is the edge list returned by DisjointSet.spanningForestEdges WeightedEdge.endpoints es.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalScan_sublist {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (es : List (WeightedEdge n W)) : (kruskalScan p es).Sublist es

kruskalScan p es is an order-preserving sublist of es.

theorem Cslib.Algorithms.Lean.Kruskal.edgePartitionFrom_kruskalScan {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (es : List (WeightedEdge n W)) : edgePartitionFrom p (kruskalScan p es) = edgePartitionFrom p es

kruskalScan p es preserves the final partition edgePartitionFrom p es.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalScan_isAcyclicFrom {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (es : List (WeightedEdge n W)) : IsAcyclicFrom p (kruskalScan p es)

kruskalScan p es is acyclic relative to p.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalScan_isSpanningForestFrom {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (es : List (WeightedEdge n W)) : IsSpanningForestFrom p es (kruskalScan p es)

kruskalScan p es is a relative spanning forest of es over p.

theorem Cslib.Algorithms.Lean.Kruskal.totalWeight_kruskalScan_le {n : ℕ} {W : Type} [AddCommMonoid W] [Preorder W] [IsOrderedAddMonoid W] (p : DataStructure.DisjointSet.Partition n) {sorted H : List (WeightedEdge n W)} (hsorted : List.Pairwise (fun (a b : WeightedEdge n W) => a.weight ≤ b.weight) sorted) (hH : IsSpanningForestFrom p sorted H) : totalWeight (kruskalScan p sorted) ≤ totalWeight H

Core exchange-inductive optimality of kruskalScan on weight-sorted inputs: for any initial partition p and any relative spanning forest H of sorted over p, kruskalScan p sorted has total weight at most totalWeight H.

theorem Cslib.Algorithms.Lean.Kruskal.perm_kruskalScan_of_totalWeight_le_of_nodup_weights {n : ℕ} {W : Type} [AddCancelCommMonoid W] [LinearOrder W] [IsOrderedCancelAddMonoid W] (p : DataStructure.DisjointSet.Partition n) {sorted H : List (WeightedEdge n W)} (hsorted : List.Pairwise (fun (a b : WeightedEdge n W) => a.weight ≤ b.weight) sorted) (hnodup : (List.map WeightedEdge.weight sorted).Nodup) (hH : IsSpanningForestFrom p sorted H) (hopt : totalWeight H ≤ totalWeight (kruskalScan p sorted)) : H.Perm (kruskalScan p sorted)

Uniqueness of the minimum relative spanning forest on weight-sorted inputs with distinct weights.

def Cslib.Algorithms.Lean.Kruskal.sortEdges {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : List (WeightedEdge n W)

Sort an edge list by nondecreasing weight using List.mergeSort.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.sortEdges_nil {n : ℕ} {W : Type} [LE W] [DecidableLE W] : sortEdges [] = []

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.sortEdges_singleton {n : ℕ} {W : Type} [LE W] [DecidableLE W] (e : WeightedEdge n W) : sortEdges [e] = [e]

theorem Cslib.Algorithms.Lean.Kruskal.sortEdges_cons_cons {n : ℕ} {W : Type} [LE W] [DecidableLE W] (a b : WeightedEdge n W) (es : List (WeightedEdge n W)) : sortEdges (a :: b :: es) = (sortEdges (List.take ((es.length + 3) / 2) (a :: b :: es))).merge (sortEdges (List.drop ((es.length + 3) / 2) (a :: b :: es))) fun (x y : WeightedEdge n W) => decide (x.weight ≤ y.weight)

Balanced-split unfolding step for sortEdges on lists of length at least 2.

theorem Cslib.Algorithms.Lean.Kruskal.sortEdges_perm {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : (sortEdges es).Perm es

sortEdges es is a permutation of es.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.sortEdges_length {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : (sortEdges es).length = es.length

theorem Cslib.Algorithms.Lean.Kruskal.sortEdges_sorted {n : ℕ} {W : Type} [LinearOrder W] (es : List (WeightedEdge n W)) : List.Pairwise (fun (a b : WeightedEdge n W) => a.weight ≤ b.weight) (sortEdges es)

Over a linear order, sortEdges es is sorted in nondecreasing weight order.

def Cslib.Algorithms.Lean.Kruskal.kruskalEdges {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : List (WeightedEdge n W)

Kruskal's algorithm: merge-sort edges in nondecreasing weight order and scan from the discrete partition Partition.discrete n, retaining each edge whose endpoints lie in distinct components.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalEdges_sorted {n : ℕ} {W : Type} [LinearOrder W] (es : List (WeightedEdge n W)) : List.Pairwise (fun (a b : WeightedEdge n W) => a.weight ≤ b.weight) (kruskalEdges es)

kruskalEdges es is sorted in nondecreasing weight order.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalEdges_subperm {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : (kruskalEdges es).Subperm es

kruskalEdges es is a sub-multiset (Subperm) of es.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalEdges_isAcyclic {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : IsAcyclic (kruskalEdges es)

kruskalEdges es is acyclic.

theorem Cslib.Algorithms.Lean.Kruskal.edgePartition_kruskalEdges {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : edgePartition (kruskalEdges es) = edgePartition es

kruskalEdges es induces the exact same connected-component partition as es.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalEdges_isSpanningForest {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : IsSpanningForest es (kruskalEdges es)

kruskalEdges es is a spanning forest of es.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalEdges_isMinSpanningForest {n : ℕ} {W : Type} [AddCommMonoid W] [LinearOrder W] [IsOrderedAddMonoid W] (es : List (WeightedEdge n W)) : IsMinSpanningForest es (kruskalEdges es)

Kruskal's minimum spanning forest theorem (generalizing Cormen et al., Section 23.2, MST-KRUSKAL, p. 631 from connected simple real-weighted graphs to arbitrary finite multigraphs): for any weighted multigraph es on Fin n with weights in an ordered additive commutative monoid, kruskalEdges es is a minimum-weight spanning forest of es.

theorem Cslib.Algorithms.Lean.Kruskal.totalWeight_kruskalEdges_le {n : ℕ} {W : Type} [AddCommMonoid W] [LinearOrder W] [IsOrderedAddMonoid W] (es : List (WeightedEdge n W)) (hnonneg : ∀ e ∈ es, 0 ≤ e.weight) : totalWeight (kruskalEdges es) ≤ totalWeight es

With nonnegative weights, Kruskal's forest weighs at most its whole input.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalEdges_isMinSpanningTree {n : ℕ} {W : Type} [AddCommMonoid W] [LinearOrder W] [IsOrderedAddMonoid W] {es : List (WeightedEdge n W)} (hconn : (edgePartition es).numComponents = 1) : IsMinSpanningTree es (kruskalEdges es)

Kruskal's minimum spanning tree theorem (Cormen et al., Section 23.2, p. 631): when es connects Fin n into a single component ((edgePartition es).numComponents = 1), kruskalEdges es is a minimum-weight spanning tree of es.

theorem Cslib.Algorithms.Lean.Kruskal.perm_kruskalEdges_of_isMinSpanningForest_of_nodup_weights {n : ℕ} {W : Type} [AddCancelCommMonoid W] [LinearOrder W] [IsOrderedCancelAddMonoid W] {es F : List (WeightedEdge n W)} (hnodup : (List.map WeightedEdge.weight es).Nodup) (hF : IsMinSpanningForest es F) : F.Perm (kruskalEdges es)

Distinct-weight uniqueness of Kruskal's forest (generalizing Kruskal, Opening paragraph, Construction A, and uniqueness proof, pp. 48–50): when all edges in es have pairwise distinct weights, every minimum-weight spanning forest of es is a permutation of kruskalEdges es (i.e., selects the exact same multiset of edges).

theorem Cslib.Algorithms.Lean.Kruskal.perm_kruskalEdges_of_isMinSpanningTree_of_nodup_weights {n : ℕ} {W : Type} [AddCancelCommMonoid W] [LinearOrder W] [IsOrderedCancelAddMonoid W] {es T : List (WeightedEdge n W)} (hconn : (edgePartition es).numComponents = 1) (hnodup : (List.map WeightedEdge.weight es).Nodup) (hT : IsMinSpanningTree es T) : T.Perm (kruskalEdges es)

Distinct-weight uniqueness specialized to connected multigraphs: when edge weights in es are pairwise distinct and es is connected, every minimum spanning tree of es is a permutation of kruskalEdges es.

DisjointSet.spec client and backend-parametric realization

def Cslib.Algorithms.Lean.Kruskal.kruskalClient {n : ℕ} {W : Type} (es : List (WeightedEdge n W)) : (DataStructure.DisjointSet.spec n).Client (List (WeightedEdge n W))

DisjointSet.spec n client for the Kruskal scan, defined as the WeightedEdge.endpoints specialization of DisjointSet.spanningForestEdges.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.eval_kruskalClient {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (es : List (WeightedEdge n W)) : DataStructure.eval (DataStructure.DisjointSet.spec n) (kruskalClient es) p = (kruskalScan p es, edgePartitionFrom p es)

eval view of kruskalClient.

theorem Cslib.Algorithms.Lean.Kruskal.runClient_kruskalClient {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (es : List (WeightedEdge n W)) : (DataStructure.DisjointSet.spec n).runClient p (kruskalClient es) = (kruskalScan p es, edgePartitionFrom p es, List.map (fun (e : WeightedEdge n W) => DataStructure.DisjointSet.Op.union e.u e.v) es)

Exact mathematical evaluation and operation history of kruskalClient: it computes kruskalScan p es, reaches edgePartitionFrom p es, and issues one Op.union e.u e.v per edge.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalScan_map_endpoints {n : ℕ} {W : Type} (p : DataStructure.DisjointSet.Partition n) (es : List (WeightedEdge n W)) : List.map WeightedEdge.endpoints (kruskalScan p es) = (DataStructure.eval (DataStructure.DisjointSet.spec n) (DataStructure.DisjointSet.spanningForestEdges id (List.map WeightedEdge.endpoints es)) p).1

Projecting endpoints of kruskalClient matches unweighted DisjointSet.spanningForestEdges id.

theorem Cslib.Algorithms.Lean.Kruskal.realized_kruskal {n : ℕ} {W : Type} [LE W] [DecidableLE W] {C τ : Type} {exec : DataStructure.Execution (DataStructure.DisjointSet.spec n).signature C τ} (R : DataStructure.StateTransitionImpl (DataStructure.DisjointSet.spec n) exec) {cost : τ → ℕ} {charge : DataStructure.DisjointSet.Partition n → DataStructure.DisjointSet.Op n → ℕ} (B : DataStructure.Bound R cost charge) {s₀ : C} (hr : R.rep (DataStructure.DisjointSet.Partition.discrete n) s₀) (es : List (WeightedEdge n W)) : ∃ (s' : C) (traces : List τ), DataStructure.Executes exec (kruskalClient (sortEdges es)) s₀ (kruskalEdges es) s' traces ∧ R.rep (edgePartition es) s' ∧ DataStructure.total cost traces ≤ (DataStructure.DisjointSet.spec n).totalCost charge (DataStructure.DisjointSet.Partition.discrete n) (List.map (fun (e : WeightedEdge n W) => DataStructure.DisjointSet.Op.union e.u e.v) (sortEdges es))

Backend-parametric Kruskal execution: for any Cslib.DataStructure.StateTransitionImpl and Cslib.DataStructure.Bound for DisjointSet.spec n, from a state representing Partition.discrete n there is an execution of kruskalClient (sortEdges es) that returns kruskalEdges es, ends in a state representing edgePartition es, and has total cost at most the total charge of its m Op.union calls.

TimeM complexity with sorting comparisons and UnionFind steps

structure Cslib.Algorithms.Lean.Kruskal.Cost : Type

Two-component cost profile for Kruskal's algorithm: edge-weight comparisons during merge sort and disjoint-set forest steps during the cycle-filtering scan.

• comparisons : ℕ

  Number of edge-weight comparisons performed while sorting edges.

• ufSteps : ℕ

  Number of disjoint-set forest steps (find parent-pointer inspections plus union root links) performed during the Kruskal scan.

theorem Cslib.Algorithms.Lean.Kruskal.Cost.ext_iff {x y : Cost} : x = y ↔ x.comparisons = y.comparisons ∧ x.ufSteps = y.ufSteps

theorem Cslib.Algorithms.Lean.Kruskal.Cost.ext {x y : Cost} (comparisons : x.comparisons = y.comparisons) (ufSteps : x.ufSteps = y.ufSteps) : x = y

@[instance_reducible]

instance Cslib.Algorithms.Lean.Kruskal.instReprCost : Repr Cost

def Cslib.Algorithms.Lean.Kruskal.instReprCost.repr : Cost → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Algorithms.Lean.Kruskal.Cost.instDecidableEq : DecidableEq Cost

def Cslib.Algorithms.Lean.Kruskal.Cost.total (c : Cost) : ℕ

Combined operation count comparisons + ufSteps.

@[instance_reducible]

instance Cslib.Algorithms.Lean.Kruskal.Cost.instZero : Zero Cost

@[instance_reducible]

instance Cslib.Algorithms.Lean.Kruskal.Cost.instAdd : Add Cost

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.Cost.comparisons_zero : comparisons 0 = 0

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.Cost.ufSteps_zero : ufSteps 0 = 0

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.Cost.total_zero : total 0 = 0

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.Cost.comparisons_add (a b : Cost) : (a + b).comparisons = a.comparisons + b.comparisons

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.Cost.ufSteps_add (a b : Cost) : (a + b).ufSteps = a.ufSteps + b.ufSteps

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.Cost.total_add (a b : Cost) : (a + b).total = a.total + b.total

@[instance_reducible]

instance Cslib.Algorithms.Lean.Kruskal.Cost.instAddCommMonoid : AddCommMonoid Cost

structure Cslib.Algorithms.Lean.Kruskal.Output (n : ℕ) (W : Type) : Type

Concrete output of kruskalM: the selected forest edges together with the final DisjointSet.UnionFind.State n representing the graph's connected components.

• forest : List (WeightedEdge n W)

  Selected spanning-forest edges.

• ufState : DataStructure.DisjointSet.UnionFind.State n

  Final concrete union-find forest state after scanning all edges.

def Cslib.Algorithms.Lean.Kruskal.liftComparisons {α : Type} (m : TimeM ℕ α) : TimeM Cost α

Lift a comparison-counting TimeM ℕ computation into TimeM Cost.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.ret_liftComparisons {α : Type} (m : TimeM ℕ α) : (liftComparisons m).ret = m.ret

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.time_liftComparisons {α : Type} (m : TimeM ℕ α) : (liftComparisons m).time = { comparisons := m.time, ufSteps := 0 }

def Cslib.Algorithms.Lean.Kruskal.sortEdgesM {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : TimeM ℕ (List (WeightedEdge n W))

Merge-sort edges by nondecreasing weight in TimeM ℕ, charging 1 per weight comparison.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.sortEdgesM_nil {n : ℕ} {W : Type} [LE W] [DecidableLE W] : sortEdgesM [] = pure []

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.sortEdgesM_singleton {n : ℕ} {W : Type} [LE W] [DecidableLE W] (e : WeightedEdge n W) : sortEdgesM [e] = pure [e]

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.ret_sortEdgesM {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : (sortEdgesM es).ret = sortEdges es

theorem Cslib.Algorithms.Lean.Kruskal.time_sortEdgesM_le {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : (sortEdgesM es).time ≤ es.length * Nat.clog 2 es.length

sortEdgesM es performs at most es.length * Nat.clog 2 es.length weight comparisons.

def Cslib.Algorithms.Lean.Kruskal.kruskalScanM {n : ℕ} {W : Type} (s : DataStructure.DisjointSet.UnionFind.State n) (sorted : List (WeightedEdge n W)) : TimeM Cost (Output n W)

Timed Kruskal scan starting from a concrete DisjointSet.UnionFind.State n, charging exact union-find forest steps to Cost.ufSteps.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.comparisons_kruskalScanM {n : ℕ} {W : Type} (s : DataStructure.DisjointSet.UnionFind.State n) (sorted : List (WeightedEdge n W)) : (kruskalScanM s sorted).time.comparisons = 0

theorem Cslib.Algorithms.Lean.Kruskal.kruskalScanM_correct {n : ℕ} {W : Type} {p : DataStructure.DisjointSet.Partition n} {s : DataStructure.DisjointSet.UnionFind.State n} (hr : DataStructure.DisjointSet.UnionFind.Rep p s) (sorted : List (WeightedEdge n W)) : (kruskalScanM s sorted).ret.forest = kruskalScan p sorted ∧ DataStructure.DisjointSet.UnionFind.Rep (edgePartitionFrom p sorted) (kruskalScanM s sorted).ret.ufState ∧ (kruskalScanM s sorted).time.ufSteps ≤ sorted.length * (2 * Nat.log 2 n + 3)

Correctness and O(log n) per-edge disjoint-set step bound for kruskalScanM.

def Cslib.Algorithms.Lean.Kruskal.kruskalM {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : TimeM Cost (Output n W)

Kruskal's minimum-spanning-forest algorithm in TimeM Cost (Cormen et al., Section 23.2, MST-KRUSKAL, pp. 631–633): merge-sort es by weight (charging comparisons to Cost.comparisons) and scan the sorted edges from DisjointSet.UnionFind.init n (charging post-initialization parent-pointer inspections and root links to Cost.ufSteps, with DisjointSet.UnionFind.init n uncharged).

theorem Cslib.Algorithms.Lean.Kruskal.kruskalM_ret {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : (kruskalM es).ret = (kruskalScanM (DataStructure.DisjointSet.UnionFind.init n) (sortEdges es)).ret

Pure return value of kruskalM es in terms of kernel-reducible sortEdges and kruskalScanM.

@[simp]

theorem Cslib.Algorithms.Lean.Kruskal.kruskalM_forest {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : (kruskalM es).ret.forest = kruskalEdges es

kruskalM es computes kruskalEdges es.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalM_isMinSpanningForest {n : ℕ} {W : Type} [AddCommMonoid W] [LinearOrder W] [IsOrderedAddMonoid W] (es : List (WeightedEdge n W)) : IsMinSpanningForest es (kruskalM es).ret.forest

Over an ordered additive commutative monoid, (kruskalM es).ret.forest is a minimum-weight spanning forest of es.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalM_rep {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : DataStructure.DisjointSet.UnionFind.Rep (edgePartition es) (kruskalM es).ret.ufState

Final union-find state invariant: (kruskalM es).ret.ufState represents edgePartition es.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalM_numComp {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : (kruskalM es).ret.ufState.numComp = (edgePartition es).numComponents

The maintained component counter of (kruskalM es).ret.ufState equals the number of connected components (edgePartition es).numComponents.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalM_comparisons_le {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : (kruskalM es).time.comparisons ≤ es.length * Nat.clog 2 es.length

Sorting comparison bound for kruskalM: at most m * ⌈log₂ m⌉ weight comparisons where m = es.length.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalM_ufSteps_le {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : (kruskalM es).time.ufSteps ≤ es.length * (2 * Nat.log 2 n + 3)

Disjoint-set forest step bound for kruskalM: at most m * (2 * ⌊log₂ n⌋ + 3) union-find steps where m = es.length.

theorem Cslib.Algorithms.Lean.Kruskal.kruskalM_total_le {n : ℕ} {W : Type} [LE W] [DecidableLE W] (es : List (WeightedEdge n W)) : (kruskalM es).time.total ≤ es.length * Nat.clog 2 es.length + es.length * (2 * Nat.log 2 n + 3)

Combined O(m log m + m log n) bound on total operations (kruskalM es).time.total.