TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-01

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Prim's growing-tree procedure produces a minimum spanning tree

Statement

Let $(G,w)$ be a connected real edge-weighted graph and choose a start vertex. Repeatedly add a minimum-weight edge with exactly one endpoint in the vertices reached so far. With ties broken arbitrarily, after all vertices are reached the chosen edges form a minimum spanning tree.

Facts & Assumptions

Given: A connected finite weighted graph $(G,w)$ and a start vertex $r$ .

[L1]

$G$ has an MST (A finite graph is connected if and only if it has a spanning tree, Real edge-weighted graphs, total tree weight and minimum spanning trees).

[L2]

A minimum edge crossing a cut belongs to some MST, and exchanging an outside edge for an edge of its fundamental cycle preserves a spanning tree (Cut and cycle properties for minimum spanning trees, The spanning-tree exchange lemma).

[F1]

A finite nonempty set of crossing-edge weights has a least member, by order duality from Every nonempty finite set of reals has a maximum and a minimum.

[L3]

Induction applies to the finite reached set (The cardinality $\lvert A\rvert$ of a finite set, The principle of mathematical induction).

[F2]

A connected acyclic spanning subgraph is a spanning tree, and an MST is a spanning tree of minimum weight (Spanning trees of a graph, Real edge-weighted graphs, total tree weight and minimum spanning trees).

Proof

technique · induction on the number of reached vertices

1.1

Maintain the invariant that the chosen edges $F$ are contained in some MST. It holds for $F=\varnothing$ by L1.

baseL1

1.2

Assume the invariant for the current reached set $S$ . If $S$ is not all of $V(G)$ , connectedness gives an edge crossing $(S,V(G)\setminus S)$ , so a minimum-weight crossing edge $e$ exists.

ihF1

2.1

Choose an MST $T$ containing $F$ . If $e\notin T$ , the $T$ -path between the endpoints of $e$ contains an edge $f$ crossing $(S,V(G)\setminus S)$ . No edge of $F$ crosses this cut, and $w(e)\le w(f)$ , so $T-f+e$ is an MST containing $F+e$ . Thus in either case some MST contains $F+e$ .

step 1.2L2

3.1

Hence the invariant persists, and adding $e$ reaches one new vertex without creating a cycle.

step 2.1L3

4.1

After all vertices are reached, $F$ is connected and acyclic with all vertices, so it is a spanning tree. Since an MST contains all its edges, it equals $F$ .

step 3.1F2

5.1

Thus Prim's procedure returns an MST for every permitted tie-breaking.

step 4.1discharge-induction∎

Depends on

Used by

Kruskal's and Prim's procedures on the same weighted graph Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 73 results over 27 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

ISI Bangalore discrete mathematics notes, Kruskal and other algorithms (standard reference, not scraped)