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.

Cut and cycle properties for minimum spanning trees

Statement

Let $(G,w)$ be a connected real edge-weighted graph.

A minimum-weight edge crossing any nontrivial cut belongs to some MST.
A uniquely minimum-weight edge crossing a cut belongs to every MST.
A maximum-weight edge on any cycle is omitted by some MST.
A uniquely maximum-weight edge on a cycle belongs to no MST.

Facts & Assumptions

Given: A connected weighted graph $(G,w)$ .

[F1]

An MST minimizes the sum of its edge weights (Real edge-weighted graphs, total tree weight and minimum spanning trees).

[L1]

Exchanging an outside edge with a suitable tree edge on its fundamental cycle, or a tree edge with a crossing edge of its fundamental cut, preserves the spanning-tree property (The spanning-tree exchange lemma, Every edge outside a spanning tree determines a unique fundamental cycle, Every edge of a spanning tree determines a fundamental cut, and every edge crossing it restores a spanning tree).

Proof

technique · direct exchange arguments

1.1

Let $e$ be a minimum edge crossing a cut and choose an MST $T$ . If $e\in T$ , this MST already proves assertion 1. If $e\notin T$ , the fundamental cycle of $e$ contains a tree edge $f$ crossing the same cut.

chooseL1

1.2

Let $g$ be a maximum edge on a cycle and choose an MST $S$ . If $g\notin S$ , this MST already proves assertion 3. If $g\in S$ , deleting $g$ gives a fundamental cut, and the remainder of the cycle contains an edge $h$ crossing that cut.

chooseL1

2.1

In the second case of step 1.1, $w(e)\le w(f)$ , so $T-f+e$ is an MST containing $e$ . Together with the first case, this proves assertion 1.

step 1.1L1F1

2.2

If $e$ is uniquely minimum across the cut and an MST omitted it, the same exchange would have $w(e)<w(f)$ and strictly decrease total weight. Thus every MST contains $e$ .

step 1.1F1

2.3

In the second case of step 1.2, $w(h)\le w(g)$ , so $S-g+h$ is an MST omitting $g$ . Together with the first case, this proves assertion 3.

step 1.2L1F1

3.1

If $g$ is uniquely maximum on the cycle, then $w(h)<w(g)$ in step 1.2, so no MST can contain $g$ .

step 1.2step 2.3F1∎

Depends on

Used by

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

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 44 results over 12 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, Minimal spanning trees (standard reference, not scraped)