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.
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.
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.
Depends on
- A finite simple graph is a finite vertex set together with a set of two-element vertex subsets
- 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
- Adjacency, incidence, open and closed neighbourhoods, vertex degree, minimum degree and maximum degree
Used by
- A tree on n≥1 vertices has n-1 edges Corollary
- Every tree with at least two vertices has at least two leaves Corollary
- An acyclic graph need not be a tree Counterexample
- Rooted trees, ancestors, descendants, depth, height, parents and children Definition
- Spanning trees of a graph Definition
- The Prüfer code of a tree on a finite set of natural labels Definition
- A maximal acyclic spanning subgraph of a connected graph is a spanning tree Lemma
- Adding an edge between two nonadjacent vertices of a tree creates exactly one cycle Lemma
- Deleting any edge of a tree separates it into exactly two tree components Lemma
- Every nonempty forest has a vertex of degree at most one Lemma
- The Prüfer decoding procedure is well defined and produces a labelled tree Lemma
- Every plane forest has exactly one face Proposition
- Equivalent characterisations of a nonempty tree by unique paths, edge count, minimal connectivity and maximal acyclicity Theorem
- For every forest, |V|=|E|+c, where c is the number of connected components Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 15 results over 11 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
- Reinhard Diestel, Graph Theory, Preview Chapter 1 (standard reference, not scraped)