Alphabeta Math
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.

✓ 21 results · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 21 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Trees, Forests and Spanning Trees

1 · Prerequisites

2 · Summary

Published finite-simple-graph conventions, path and cycle definitions, connected components, vertex degrees, graph deletion, and finite-cardinality results supply the structural setting. Forest component counting gives ∣V∣=∣E∣+c, while deleting a tree edge or adding a missing edge relates acyclicity, connectivity, unique paths, and the tree edge count.

Those structural equivalences lead to rooted-tree levels, spanning trees, fundamental cycles and cuts, and the finite spanning-tree number. Prüfer encoding and decoding then biject labelled trees with words and yield Cayley's formula. For real edge weights, spanning-tree exchange proves cut and cycle rules, uniqueness under distinct weights, and correctness of Kruskal's and Prim's finite greedy procedures.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-01Open item page →

Trees, forests, leaves and isolated vertices

Definition

All graphs here are finite, simple and undirected (A finite simple graph is a finite vertex set together with a set of two-element vertex subsets). A forest is a graph containing no cycle, and a tree is a connected forest (Walks, closed walks, trails, paths and cycles, with length equal to the number of traversed edges, Connected graphs and connected components defined by the existence of vertex paths).

A vertex of degree one is a leaf. A vertex of degree zero is isolated (Adjacency, incidence, open and closed neighbourhoods, vertex degree, minimum degree and maximum degree). Thus the one-vertex tree has an isolated vertex and no leaf under this convention. A nontrivial tree means a tree with at least two vertices.

vleafT1T2isolatedforestF:componentsT1,T2,K1

Remarks

  • The null graph is a forest but not a tree, because it is not connected under the library convention.
  • Every connected component of a nonnull forest is a tree.
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-01Open item page →

Every nonempty forest has a vertex of degree at most one

Statement

Every forest with at least one vertex has a vertex of degree at most one.

Facts & Assumptions

Given: A forest F with V(F)≠∅.

[L1]

A forest contains no cycle (Trees, forests, leaves and isolated vertices).

[L2]

Every finite graph of minimum degree at least two contains a cycle (Every finite simple graph of minimum degree at least two contains a cycle).

Proof

technique · contradiction
1.1

Suppose every vertex of F has degree greater than one.

assume-contra
2.1

Since degrees are natural numbers, F has minimum degree at least two.

step 1.1F1
3.1

Hence F contains a cycle.

step 2.1L2
4.1

This contradicts that F is a forest, so some vertex has degree at most one.

step 3.1L1discharge-contradiction∎
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-01Open item page →

For every forest, ∣V∣=∣E∣+c, where c is the number of connected components

Statement

If F is a forest, let C(F) be the family of vertex sets of its connected components and put c(F):=∣C(F)∣. Then

∣V(F)∣=∣E(F)∣+c(F).

For the null forest, c(F)=0.

Facts & Assumptions

Proof

technique · induction on $|V(F)|$
1.1

If ∣V(F)∣=0, then ∣E(F)∣=0 and c(F)=0, so the identity holds.

base
1.2

Let ∣V(F)∣>0, assume the identity for forests with fewer vertices, and choose a vertex v of degree at most one.

ihL1L3
2.1

Put F′:=F−v. It remains a forest, and V(F) is the disjoint union of V(F′) and {v}, so ∣V(F)∣=∣V(F′)∣+1.

step 1.2L1F1F2
3.1

If v is isolated, then E(F)=E(F′), while the component family of F is the disjoint union of the component family of F′ and {{v}}. Hence ∣E(F)∣=∣E(F′)∣ and c(F)=c(F′)+1.

step 2.1F1L2F2
3.2

If v has degree one, deleting it removes its unique incident edge, so ∣E(F)∣=∣E(F′)∣+1. It does not change the number of components: v cannot be an internal vertex of a path between remaining vertices, and its neighbour remains in the same nonempty component after deletion. Thus c(F)=c(F′).

step 2.1F1L2F2
4.1

In the isolated case, the induction hypothesis gives ∣V(F)∣=∣V(F′)∣+1=(∣E(F′)∣+c(F′))+1=∣E(F)∣+c(F).

step 1.2step 2.1step 3.1F2
4.2

In the degree-one case, the induction hypothesis gives ∣V(F)∣=∣V(F′)∣+1=(∣E(F′)∣+c(F′))+1=(∣E(F′)∣+1)+c(F′)=∣E(F)∣+c(F).

step 1.2step 2.1step 3.2F2
5.1

The two possible degrees of v have both been handled, so the identity holds for every forest.

step 4.1step 4.2discharge-induction∎
CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-01Open item page →

A tree on n≥1 vertices has n−1 edges

Statement

A tree with n≥1 vertices has exactly n−1 edges.

Facts & Assumptions

Given: A tree T with ∣V(T)∣=n.

[F1]

A tree is connected and acyclic, so it is a forest with exactly one connected component (Trees, forests, leaves and isolated vertices, Connected graphs and connected components defined by the existence of vertex paths).

Proof

technique · direct
1.1

Apply the forest identity to T: n=∣E(T)∣+1.

L1F1
2.1

Therefore ∣E(T)∣=n−1.

step 1.1∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-01Open item page →

Deleting any edge of a tree separates it into exactly two tree components

Statement

If T is a tree and e=uv∈E(T), then T−e has exactly two connected components, each of which is a tree.

Facts & Assumptions

Given: A tree T and an edge e=uv.

[F1]

A tree is connected and has no cycle (Trees, forests, leaves and isolated vertices).

[F2]

T−e has the same vertices and all edges of T except e (Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors).

Proof

technique · direct
1.1

The vertices u and v lie in distinct components of T−e: otherwise a u-v path in T−e together with e would be a cycle in T.

F1F2F3
1.2

Every vertex x lies in the component of u or the component of v. Indeed, take an x-u path in T; if it avoids e it joins x to u in T−e, and if it uses e then its segment from x to v avoids e.

F1F2F3
2.1

Thus T−e has exactly two components.

step 1.1step 1.2
3.1

Each component is connected by definition and contains no cycle because it is a subgraph of the acyclic graph T. Hence each component is a tree.

F1F3∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

Adding an edge between two nonadjacent vertices of a tree creates exactly one cycle

Statement

Let T be a tree and let u,v be nonadjacent vertices. Adding the edge uv creates exactly one cycle.

Facts & Assumptions

Given: A tree T and nonadjacent vertices u,v∈V(T).

[F1]

A tree is connected and acyclic (Trees, forests, leaves and isolated vertices).

Proof

technique · direct
1.1

There is a u-v path P in T, and it is unique: if two distinct such paths existed, their first divergence and next reunion would yield a cycle.

F1F2
1.2

Every cycle in T+uv must contain uv, since T itself is acyclic. Removing uv from such a cycle leaves a u-v path in T.

F1F2
2.1

The path P together with the new edge uv is a cycle in T+uv.

step 1.1F2
3.1

By uniqueness in step 1.1, the path obtained in step 1.2 is P. Hence the cycle in step 2.1 is the only cycle.

step 1.1step 1.2∎
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-01Open item page →

Equivalent characterisations of a nonempty tree by unique paths, edge count, minimal connectivity and maximal acyclicity

Statement

For a finite nonempty graph G, the following are equivalent:

  1. G is a tree.
  2. Every two vertices are joined by a unique path.
  3. G is connected and ∣E(G)∣=∣V(G)∣−1.
  4. G is acyclic and ∣E(G)∣=∣V(G)∣−1.
  5. G is minimally connected: it is connected, but deleting any edge disconnects it.
  6. G is maximally acyclic: it is acyclic, but adding any missing edge creates a cycle.

Facts & Assumptions

Given: A finite nonempty graph G.

[L1]

Forests satisfy ∣V∣=∣E∣+c, and trees satisfy ∣E∣=∣V∣−1 (For every forest, ∣V∣=∣E∣+c, where c is the number of connected components, A tree on n≥1 vertices has n−1 edges).

[L2]
[F1]

A tree is connected and acyclic (Trees, forests, leaves and isolated vertices).

Proof

technique · direct cycle of implications
1.1

If G is a tree, connectedness supplies a path between each two vertices, and two distinct paths would contain a cycle. Thus condition 1 implies condition 2.

F1F2
1.2

Under condition 2, G is connected. Deleting any edge uv leaves no u-v path, because such a path together with uv would give a second path in G. Thus condition 2 implies condition 5.

F2
1.3

Suppose condition 5 holds. If G contained a cycle, deleting one edge of that cycle would leave its endpoints joined around the rest of the cycle and would not disconnect G. Hence G is acyclic and therefore is a tree. Thus condition 5 implies condition 1.

F2F1
1.4

Condition 1 implies condition 3 by the tree edge count.

L1
1.5

Under condition 3, suppose G had a cycle. Repeatedly delete an edge from a cycle; each deletion preserves connectedness, and finiteness makes the process stop at a connected acyclic spanning graph T. At least one edge was deleted, so ∣E(T)∣<∣V(G)∣−1, while the forest identity with one component gives ∣E(T)∣=∣V(G)∣−1, a contradiction. Hence condition 3 implies condition 1.

L1F2
1.6

Under condition 4, the forest identity gives ∣V∣=(∣V∣−1)+c, so c=1 and G is a tree. Conversely condition 1 implies condition 4 by definition and the tree edge count.

L1F1
1.7

Condition 1 implies condition 6 by edge addition.

L2
1.8

Under condition 6, if G were disconnected, vertices in different components would be nonadjacent and adding an edge between them could create no cycle. Hence G is connected, and its assumed acyclicity makes it a tree.

F1F2
2.1

All six conditions are therefore equivalent.

step 1.1step 1.2step 1.3step 1.4step 1.5step 1.6step 1.7step 1.8∎
CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-01Open item page →

Every tree with at least two vertices has at least two leaves

Statement

Every tree with at least two vertices has at least two distinct leaves.

Proof

technique · direct
1.1

Choose a path P=v0v1⋯vk of maximum length. Since T has at least two vertices and is connected, k≥1.

F2L1
2.1

If v0 had a neighbour other than v1, that neighbour could not already lie on P, since that would form a cycle; adjoining it would therefore lengthen the maximum-length path P. Thus v0 has degree one.

step 1.1L1
2.2

The same argument shows that vk has degree one.

step 1.1L1
3.1

Since v0≠vk, these are two distinct leaves.

step 1.1step 2.1step 2.2F1∎
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-01Open item page →

Rooted trees, ancestors, descendants, depth, height, parents and children

Definition

A rooted tree is a pair (T,r) consisting of a tree T and a distinguished vertex r, the root (Trees, forests, leaves and isolated vertices). The unique r-v path is the root path of v (Equivalent characterisations of a nonempty tree by unique paths, edge count, minimal connectivity and maximal acyclicity).

The depth of v is dT(r,v), and the height of (T,r) is the maximum vertex depth (Graph distance within a component, eccentricity, diameter and girth, including the acyclic convention). A vertex u is an ancestor of v, and v a descendant of u, when u lies on the root path of v. If v≠r, the neighbour of v immediately preceding it on its root path is its parent; the vertices having parent v are the children of v.

The vertices of depth k form level k. The root has depth zero and is its own ancestor, but it has no parent.

level0level1level2ruwvxyrootuisparentofv
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-01Open item page →

Every nonroot vertex has a unique parent, and adjacent vertices have depths differing by one

Statement

In a rooted tree (T,r), every vertex other than r has exactly one parent. If uv∈E(T), then the depths of u and v differ by exactly one.

Proof

technique · direct
1.1

For v≠r, its unique root path has positive length and therefore has one vertex immediately before v. This vertex is the unique parent of v.

L1F1
1.2

Let uv be an edge. The root paths of u and v cannot diverge before their endpoints, since the two divergent tails together with uv would form a cycle. Hence one root path is obtained from the other by appending uv.

L1
2.1

Their lengths, and therefore their depths, differ by exactly one.

step 1.2F1∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-01Open item page →

Spanning trees of a graph

Definition

Let G be a graph. A spanning tree of G is a spanning subgraph T of G that is a tree (Subgraphs, induced subgraphs and spanning subgraphs, Trees, forests, leaves and isolated vertices). Equivalently,

V(T)=V(G),E(T)⊆E(G),

and T is connected and acyclic.

The null graph has no spanning tree under the library convention that a tree is nonempty and connected.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-01Open item page →

A maximal acyclic spanning subgraph of a connected graph is a spanning tree

Statement

Let G be a finite connected graph. If F is an acyclic spanning subgraph of G maximal under edge inclusion among such subgraphs, then F is a spanning tree of G.

Facts & Assumptions

Given: A connected graph G and an edge-maximal acyclic spanning subgraph F.

[F2]

A spanning tree is a connected acyclic spanning subgraph (Spanning trees of a graph, Trees, forests, leaves and isolated vertices).

Proof

technique · contradiction
1.1

Suppose F is disconnected, and choose vertices u,v in distinct components of F.

assume-contraF1
1.2

A u-v path in G has a first edge xy whose endpoints lie in distinct components of F.

F3F1
2.1

Adding xy to F cannot create a cycle, because a cycle through xy would contain an x-y path already in F, contrary to the choice of distinct components.

step 1.2
3.1

Thus F+xy is a strictly larger acyclic spanning subgraph, contradicting maximality.

step 2.1
4.1

Hence F is connected, and therefore it is a spanning tree.

F2discharge-contradiction∎
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-01Open item page →

A finite graph is connected if and only if it has a spanning tree

Statement

A finite graph G is connected if and only if it has a spanning tree.

Facts & Assumptions

Given: A finite graph G.

[L1]

Every maximal acyclic spanning subgraph of a connected graph is a spanning tree (A maximal acyclic spanning subgraph of a connected graph is a spanning tree).

[F1]

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

[F2]

A finite graph has only finitely many edge subsets, so the family of acyclic spanning subgraphs has a maximal member.

[F3]

A graph is connected when every two vertices are joined by a path (Connected graphs and connected components defined by the existence of vertex paths).

Proof

technique · direct
1.1

If G is connected, choose a maximal acyclic spanning subgraph F; the edgeless spanning subgraph shows that the choice family is nonempty.

F2
2.1

By L1, F is a spanning tree of G.

step 1.1L1
3.1

Conversely, if G has a spanning tree T, every two vertices are joined by a path in T, hence by a path in G. Thus G is connected.

F1F3∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-01Open item page →

Every edge outside a spanning tree determines a unique fundamental cycle

Statement

If T is a spanning tree of G and e=uv∈E(G)∖E(T), then T+e has a unique cycle, namely e together with the unique u-v path in T. This is the fundamental cycle of e with respect to T.

Facts & Assumptions

Given: A spanning tree T of G and e=uv∉E(T).

[L2]

Adding an edge between nonadjacent vertices of a tree creates exactly one cycle (Adding an edge between two nonadjacent vertices of a tree creates exactly one cycle).

[F1]

T contains every vertex of G (Spanning trees of a graph).

Proof

technique · direct
1.1

The endpoints u,v belong to T and are nonadjacent there.

GivenF1
2.1

Let P be the unique u-v path in T. By edge addition, P+e is the unique cycle in T+e.

step 1.1L1L2∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

Every edge of a spanning tree determines a fundamental cut, and every edge crossing it restores a spanning tree

Statement

Let T be a spanning tree of G and e∈E(T). The two components A,B of T−e determine the fundamental cut

δT(e):={xy∈E(G):x∈A, y∈B}.

For every f∈δT(e), the graph T−e+f is a spanning tree of G.

Facts & Assumptions

Given: A spanning tree T of G and e∈E(T).

[L1]
[F2]

A spanning tree contains every vertex of G (Spanning trees of a graph).

Proof

technique · direct
1.1

Let A,B be the vertex sets of the two components of T−e. They partition V(G).

L1F2
2.1

If f=xy crosses from A to B, then T−e+f is connected: paths inside A and B, together with f, join every pair of vertices.

step 1.1L1
2.2

It is acyclic: each side is acyclic, and a cycle using f would require a second edge between the two sides, but T−e+f has only f.

step 1.1L1
3.1

It is spanning by construction, so it is a spanning tree of G.

step 2.1step 2.2F2∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-01Open item page →

The set of spanning trees of a finite graph is finite

Statement

Every finite graph has only finitely many spanning trees.

Facts & Assumptions

Given: A finite graph G.

[F1]

A spanning tree of G is determined by its edge set, which is a subset of E(G) (Spanning trees of a graph).

Proof

technique · direct
1.1

The map sending a spanning tree to its edge set embeds the set of spanning trees into P(E(G)).

F1
2.1

The latter power set is finite, so its subset consisting of spanning-tree edge sets is finite.

F2L1∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-01Open item page →

The spanning-tree number τ(G)

Definition

For a finite graph G, its spanning-tree number is

τ(G):=∣{T:T is a spanning tree of G}∣.

This is a natural number because the displayed set is finite (The set of spanning trees of a finite graph is finite, The cardinality ∣A∣ of a finite set). In particular, τ(G)=0 exactly when G has no spanning tree.

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-01Open item page →

The Prüfer code of a tree on a finite set of natural labels

Definition

Let S⊆N be finite with ∣S∣=n≥2, and let T be a tree whose vertex set is S. Here n−2 denotes the unique natural number m satisfying m+2=n. The Prüfer code is the word of length n−2 on S obtained by repeating the following operation until two vertices remain:

  1. choose the least labelled leaf v;
  2. record the unique neighbour of v;
  3. delete v and its incident edge.

A nontrivial tree has a leaf, so the least one exists (Every tree with at least two vertices has at least two leaves, The well-ordering principle). Deleting a leaf from a tree with at least three vertices leaves a tree: paths between the remaining vertices never need the deleted leaf, and no cycle is introduced. Thus every stage is defined. Each stage removes one vertex, so precisely n−2 symbols are recorded.

The usual formulation has S=n={0,1,…,n−1}, using natural numbers as their von Neumann initial segments (The natural numbers N (von Neumann), The cardinality ∣A∣ of a finite set). Allowing an arbitrary finite subset of natural labels is essential because every intermediate label set produced by deletion is again such a subset.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-01Open item page →

The Prüfer decoding procedure is well defined and produces a labelled tree

Statement

Let S⊆N be finite with ∣S∣=n≥2, and let (ai)i<n−2 be a word on the label set S. The following procedure is well defined and produces a tree on S:

At stage i, choose the least unused label absent from the remaining word ai⋯an−3, join it to ai, and mark it used. After all symbols are processed, join the two unused labels.

Facts & Assumptions

Given: A word (ai)i<n−2 on a finite set S⊆N of cardinality n≥2 (The cardinality ∣A∣ of a finite set).

[L1]

A word with r positions cannot contain more than r distinct labels. Thus among r+2 available labels at least two are absent; every nonempty set of natural labels has a least element (The pigeonhole principle on N, The well-ordering principle).

[F1]

A tree is a connected acyclic graph (Trees, forests, leaves and isolated vertices).

[L2]

Induction applies to the decoding stages (The principle of mathematical induction).

Proof

technique · induction on the stage number
1.1

Before any word entry is processed, the graph has n singleton components indexed by S, each containing exactly one unused label.

base
1.2

Assume that after i stages the built edges form a forest and every component contains exactly one unused label.

ih
2.1

There are n−i unused labels and n−2−i entries in the remaining word. Hence at least two unused labels are absent from that word, so the least such label v exists. Every label used at an earlier stage was absent from the then-remaining word and hence from its current suffix, so ai is unused; because ai occurs in the remaining word, v≠ai.

step 1.2L1
3.1

The label ai lies in a component different from the component containing v: by the induction hypothesis each component contains exactly one unused label, and ai≠v. Adding vai and marking v used joins those components without a cycle and leaves exactly one unused label in the new component. Thus the invariant holds after stage i+1.

step 1.2step 2.1
4.1

Induction gives the invariant after all n−2 word stages. Exactly two unused labels and two components remain; joining those labels makes the graph connected without creating a cycle.

step 3.1L2
5.1

The output uses all labels in S and is connected and acyclic, hence is a labelled tree on S.

step 4.1F1discharge-induction∎
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-01Open item page →

Prüfer encoding and decoding are inverse bijections between labelled trees on n≥2 vertices and words of length n−2 on their labels

Statement

For every natural n≥2, Prüfer encoding is a bijection from the set of trees with vertex set n to the set of words of length n−2 on n. Its inverse is the decoding procedure of The Prüfer decoding procedure is well defined and produces a labelled tree.

Facts & Assumptions

Given: A natural number n≥2.

[F1]

Encoding repeatedly removes the least labelled leaf and records its neighbour (The Prüfer code of a tree on a finite set of natural labels).

[L1]

Decoding is well defined and produces a labelled tree (The Prüfer decoding procedure is well defined and produces a labelled tree).

[F2]

Two maps are inverse bijections when both composites are identity maps (Injection, surjection, bijection).

[L2]

Induction is valid on the word length (The principle of mathematical induction).

[F3]

Decoding chooses the least unused label absent from the remaining word, attaches it to the first remaining symbol, and then deletes that symbol.

Proof

technique · induction on the size of the label set. We prove the stronger statement for every finite set of natural labels with its inherited order
1.1

On a two-element natural-label set, the only word is empty and the only tree is the edge joining the labels, so encoding and decoding agree.

baseF1L1
1.2

Assume that encoding and decoding are inverse on every finite natural-label set of size n−1.

ih
1.3

Let w=a0⋯an−3 and let v be the least label absent from w. Decoding first attaches v to a0 and never uses v again.

chooseF3L1
1.4

Conversely, let T be a labelled tree, let its first encoding operation delete the least leaf u, and let it record the neighbour b.

chooseF1
2.1

In the decoded tree, v is a leaf. Every label smaller than v occurs in w, so while it is unused it receives an edge as a recorded neighbour and later receives its deletion edge or the final edge. Hence no smaller label is initially a leaf, and encoding first deletes v and records a0.

step 1.3F1
2.2

The label u is absent from the full code. Every smaller label is not initially a leaf, so before it can be deleted, deletion of an incident leaf records it at least once. Thus u is the least label absent from the code, and decoding first restores the edge ub.

step 1.4F3
3.1

After removing v and the first word entry, both procedures operate on the same ordered label set of size n−1 and the suffix word. The induction hypothesis shows that the remaining operations are inverse. Thus encoding the decoded tree returns w.

step 1.2step 2.1L2
3.2

After deleting u and the first code entry, the induction hypothesis restores the remaining tree on its ordered label set of size n−1. Therefore decoding the code of T returns T.

step 1.2step 2.2L2
4.1

Both composites are identities, so encoding and decoding are inverse bijections on the ordered label set of size n. Applying this to the natural order on n proves the theorem.

step 3.1step 3.2F2discharge-induction∎
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-01Open item page →

Cayley's formula: τ(Kn)=nn−2 for n≥2, with τ(K1)=1 and τ(K0)=0

Statement

For n≥2, the complete graph Kn has

τ(Kn)=nn−2

spanning trees. Moreover, τ(K1)=1 and τ(K0)=0.

Facts & Assumptions

Proof

technique · direct
1.1

For n≥2, spanning trees of Kn are exactly the trees on its fixed label set.

F1
2.1

By the Prüfer bijection, they correspond to functions from an (n−2)-element position set to n, of which there are nn−2.

step 1.1L1L2
3.1

The sole spanning tree of K1 is K1 itself, so τ(K1)=1. The null graph K0 is not a tree and has no spanning tree, so τ(K0)=0.

F1∎
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-01Open item page →

Real edge-weighted graphs, total tree weight and minimum spanning trees

Definition

A real edge-weighted graph is a pair (G,w), where G is a finite graph and w:E(G)→R. For a spanning tree T of G, its total weight is

w(T):=∑e∈E(T)w(e)

(Spanning trees of a graph, The sum ∑i∈Sai 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 T satisfying w(T)≤w(S) for every spanning tree S of G.

If G 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 G is disconnected, it has no spanning tree and hence no MST.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-01Open item page →

The spanning-tree exchange lemma

Statement

Let T be a spanning tree of G.

  1. If e∈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.
  2. If f∈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∉T (Every edge outside a spanning tree determines a unique fundamental cycle).

[L2]

Removing f∈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∉E(T) and f≠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∎
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-01Open item page →

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∎
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

A connected graph with pairwise distinct edge weights has a unique minimum spanning tree

Statement

If a connected graph has pairwise distinct real edge weights, then it has exactly one minimum spanning tree.

Facts & Assumptions

Given: A connected weighted graph (G,w) whose edge weights are pairwise distinct.

[L2]

Exchanging an outside edge for an edge on its fundamental cycle preserves the spanning-tree property (The spanning-tree exchange lemma).

[L3]

Adding an edge outside a spanning tree creates its unique fundamental cycle (Every edge outside a spanning tree determines a unique fundamental cycle).

[F2]

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

Proof

technique · contradiction
1.1

Suppose T and T′ are distinct MSTs. Choose the least-weight edge e in the symmetric difference E(T)△E(T′), and assume after swapping names that e∈E(T)∖E(T′).

assume-contraF2
1.2

By [L3], T′+e has a fundamental cycle. Apart from e, that cycle cannot consist entirely of edges of T, since then it would be a cycle in T. Hence it contains an edge f∈E(T′)∖E(T).

chooseL3
2.1

The choice of e and distinct weights gives w(e)<w(f).

step 1.1step 1.2
3.1

The exchange T′−f+e is a spanning tree of weight w(T′)−w(f)+w(e)<w(T′), contradicting the minimality of T′.

step 1.2step 2.1L2F1
4.1

Hence the MST is unique.

step 3.1F1discharge-contradiction∎
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-01Open item page →

Kruskal's greedy edge procedure produces a minimum spanning tree

Statement

Let (G,w) be a connected real edge-weighted graph. Start with the edgeless spanning forest, repeatedly add a minimum-weight edge whose addition creates no cycle, and stop when no such edge remains. With ties broken arbitrarily, the output is a minimum spanning tree.

Facts & Assumptions

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

[L2]

Spanning-tree exchanges preserve spanning trees (The spanning-tree exchange lemma).

[L3]

Induction is valid over the finitely many chosen edges (The cardinality ∣A∣ of a finite set, The principle of mathematical induction).

[L4]

Adding an edge outside a spanning tree creates a unique fundamental cycle (Every edge outside a spanning tree determines a unique fundamental cycle).

[F1]

G is connected, and a connected acyclic spanning subgraph is a spanning tree.

[F2]

Kruskal chooses a least-weight edge among the currently eligible edges.

Proof

technique · induction on the number of chosen edges
1.1

Maintain the invariant that the current forest F is contained in some MST. It holds initially by L1.

baseL1
1.2

Suppose F⊆T for an MST T, and Kruskal chooses e. If e∈T, the invariant persists.

ih
2.1

If e∉T, let C be its fundamental cycle in T+e. Some edge f∈E(C)∖{e} is not in F; otherwise the T-path C−e would lie in F and adding e to F would create a cycle. Since F+f is a subgraph of the acyclic tree T, the edge f is eligible for Kruskal.

step 1.2L4
3.1

At the moment e is chosen, f is eligible, so w(e)≤w(f). The exchange T−f+e is a spanning tree of no greater weight, hence an MST containing F+e.

step 2.1L2F2
4.1

Thus the invariant holds after every choice.

step 1.2step 3.1L3
5.1

On termination, F must be connected: otherwise a path of G between two components of F would contain a first edge joining distinct components, and that edge would still be eligible. Thus F is a spanning tree. The invariant then forces F itself to be an MST.

step 4.1F1L1
6.1

Therefore every tie-breaking execution returns a minimum spanning tree.

step 5.1discharge-induction∎
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-01Open item page →

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.

[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.

[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=∅ 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)∖S), so a minimum-weight crossing edge e exists.

ihF1
2.1

Choose an MST T containing F. If e∉T, the T-path between the endpoints of e contains an edge f crossing (S,V(G)∖S). No edge of F crosses this cut, and w(e)≤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∎

5 · Examples, counterexamples and false statements

None yet.

Sources