Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck 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.

  1. A minimum-weight edge crossing any nontrivial cut belongs to some MST.
  2. A uniquely minimum-weight edge crossing a cut belongs to every MST.
  3. A maximum-weight edge on any cycle is omitted by some MST.
  4. 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∈T, this MST already proves assertion 1. If e∉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∉S, this MST already proves assertion 3. If g∈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)≤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)≤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

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources