Alphabeta MathHow 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.
Real edge-weighted graphs, total tree weight and minimum spanning trees
Definition
A real edge-weighted graph is a pair , where is a finite graph and . For a spanning tree of , its total weight is
(Spanning trees of a graph, The sum over a finite index set, and its product form, The reals form a totally ordered field). A minimum spanning tree, or MST, is a spanning tree satisfying for every spanning tree of .
If is connected, an MST exists: connectedness supplies a spanning tree, and the set of spanning trees is finite, so the finite nonempty set of their real weights has a least element. This is the order-dual form of the finite-set maximum principle (A finite graph is connected if and only if it has a spanning tree, The set of spanning trees of a finite graph is finite, Every nonempty finite set of reals has a maximum and a minimum). If is disconnected, it has no spanning tree and hence no MST.
Depends on
- Spanning trees of a graph
- The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form
- The reals form a totally ordered field
- The set of spanning trees of a finite graph is finite
- A finite graph is connected if and only if it has a spanning tree
- Every nonempty finite set of reals has a maximum and a minimum
Used by
- A connected graph with pairwise distinct edge weights has a unique minimum spanning tree Corollary
- A weighted graph with two distinct minimum spanning trees Counterexample
- Kruskal's and Prim's procedures on the same weighted graph Example
- Cut and cycle properties for minimum spanning trees Theorem
- Kruskal's greedy edge procedure produces a minimum spanning tree Theorem
- Prim's growing-tree procedure produces a minimum spanning tree Theorem
Dependency tree · two levels
33 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)