LemmaStatement: 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.

The spanning-tree exchange lemma

Statement

Let $T$ be a spanning tree of $G$ .

If $e \in E (G) ∖ E (T)$ and $f$ is any edge other than $e$ on the fundamental cycle of $e$ , then $T - f + e$ is a spanning tree.
If $f \in E (T)$ and $e$ crosses the fundamental cut of $f$ , then $T - f + e$ is a spanning tree.

Facts & Assumptions

Given: A graph $G$ and a spanning tree $T$ .

[L1]

$T + e$ has one fundamental cycle for every $e \notin T$ (Every edge outside a spanning tree determines a unique fundamental cycle).

[L2]

Removing $f \in T$ gives a fundamental cut, and adding any crossing edge restores a spanning tree (Every edge of a spanning tree determines a fundamental cut, and every edge crossing it restores a spanning tree).

[F1]

A spanning tree is a connected acyclic spanning subgraph (Spanning trees of a graph).

Proof

technique · constructive

1.1

Construct $T^{'} : = T - f + e$ , where $e \notin E (T)$ and $f \neq e$ lies on the fundamental cycle of $e$ . Removing $f$ breaks that cycle but leaves the graph connected, because the rest of the cycle replaces every use of $f$ .

constructL1

2.1

No other cycle exists in $T + e$ , so $T - f + e$ is connected, acyclic and spanning, hence a spanning tree.

step 1.1L1F1

3.1

The second assertion is exactly the restoration clause for the fundamental cut of $f$ .

L2discharge-construct∎

Depends on

Used by

Dependency tree · two levels

8 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

ISI Bangalore discrete mathematics notes, Minimal spanning trees (standard reference, not scraped)