Trees: deciding that a 6-vertex graph is a tree, with its leaves, a unique path and the unique cycle after adding an edge

Goal and scope

Let G=(V,E) with V={1,2,3,4,5,6} and E={{1,2},{2,3},{2,4},{4,5},{4,6}}. (1) Prove from the MKO's definition that G is a tree (V nonempty, connected, no simple cycle); (2) list its leaves; (3) find the path from 3 to 6 and prove it is unique; (4) add the edge {3,6}, write the simple cycle it creates and prove it is the only simple cycle; (5) contrast: a triangle plus an isolated vertex has |E|=|V|−1 but is not a tree; a single vertex without edges is a tree with no leaf.

Treats finite simple undirected graphs only (MKO assumption a1), with one concrete 6-vertex graph as the main example. Connectivity is proved with the lemma 'a walk contains a path', and acyclicity by deleting leaves one at a time with the lemma 'a vertex of degree at most 1 lies on no simple cycle'; both lemmas are proved here. Uniqueness of the path from 3 to 6 is proved for this example only, by exhaustion; the general theorems 'any two vertices of a tree have a unique path' and 'a tree has |V|−1 edges' are not proved here. The canonical MKO and its English edition are not changed.

Givens and symbols

• graph_basics
• well_ordering
• nat_induction
• numeric_evaluation

• G1 — G=(V,E) with V={1,2,3,4,5,6} and E={{1,2},{2,3},{2,4},{4,5},{4,6}}; edges are undirected and each is listed once.
• G2 — The MKO's path conventions: a path repeats no vertex; the zero-edge path from a vertex to itself is valid. A leaf is a vertex of degree exactly 1.
• G3 — Contrast graphs: H=({1,2,3,4},{{1,2},{2,3},{1,3}}) and K=({7},∅).

• G=(V,E) — the main example graph
• N(v),\ \deg(v) — neighbour set and degree
• (v_0,v_1,v_2) — a path or cycle written as its vertex sequence
• G-v — delete the vertex v and the edges containing it
• G+e — add the new edge e
• H,\ K — the two contrast graphs

Rules and sources

• graph_basics · prerequisite — (Simple undirected) graph: G=(V,E), where each edge is an unordered pair of distinct vertices; the degree of a vertex is the number of edges at it; handshake lemma Σ_v deg(v)=2|E|.
• well_ordering · prerequisite — Well-ordering principle: every nonempty subset of ℕ has a least element.
• nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• mko_tree_def · cited — In a finite simple undirected graph G=(V,E), a tree is a graph with V nonempty, every pair of vertices joined by a path, and no simple cycle; a leaf is a vertex of degree exactly 1. · mko-tree
• walk_path_cycle · prerequisite — A walk of length k is a sequence of vertices w_0, w_1 and so on up to w_k in which each consecutive pair w_{j−1}, w_j is an edge; a path is a walk with no repeated vertex (k=0 allowed); a simple cycle is a walk of length k≥3 with w_k=w_0 and w_0 to w_{k−1} pairwise distinct.
• delete_vertex · prerequisite — G−v has vertex set V∖{v} and the edges of E not containing v; every walk, path or cycle of G−v is also one of G.
• L_walk_path · lemma — If a graph has a walk from u to v, it has a path from u to v.
• L_leaf_cycle · lemma — If deg_G(v)≤1, then G has a simple cycle ⇔ G−v has a simple cycle.

Main derivation

G\ \text{is a tree}

V\neq\varnothing\ \land\ \forall u,v\in V\ \exists\ \text{path}\ u\to v\ \land\ \neg\exists\ \text{simple cycle}

E=\{\{1,2\},\{2,3\},\{2,4\},\{4,5\},\{4,6\}\}

G\ \text{finite simple},\ |V|=6,\ |E|=5,\ V\neq\varnothing

N(v)\ \text{for}\ v\in V

\deg(1),\deg(2),\deg(3),\deg(4),\deg(5),\deg(6)=1,3,1,3,1,1

\{v\in V:\ \deg(v)=1\}

\{1,3,5,6\}

\text{vertex}\ 1

(1),\ (1,2),\ (1,2,3),\ (1,2,4),\ (1,2,4,5),\ (1,2,4,6)

\forall u,v\in V:\ \text{walk}\ u\to 1\to v

\forall u,v\in V\ \exists\ \text{path}\ u\to v

G\ \text{has a simple cycle}

G_1=(\{2,4\},\{\{2,4\}\})\ \text{has a simple cycle}

G_1=(\{2,4\},\{\{2,4\}\})\ \text{has a simple cycle}

(\{4\},\varnothing)\ \text{has a simple cycle}

G\ \text{has a simple cycle}\iff(\{4\},\varnothing)\ \text{has one}

G\ \text{has no simple cycle}

V\neq\varnothing,\ \text{connected},\ \text{no simple cycle}

G\ \text{is a tree}

3,\ 6\in V

(3,2,4,6)\ \text{is a path from 3 to 6}

P\ \text{any path from 3 to 6}

P=(3,2,4,6)

e=\{3,6\}

3,6\in V,\ 3\neq 6,\ e\notin E;\ G+e=(V,\,E\cup\{e\})

(3,2,4,6)\ \text{in}\ G,\ e=\{6,3\}

C=(3,2,4,6,3)\ \text{is a simple cycle in}\ G+e

D\ \text{any simple cycle in}\ G+e

D=C\ \text{up to starting point and direction}

H=(\{1,2,3,4\},\{\{1,2\},\{2,3\},\{1,3\}\})

|E_H|=|V_H|-1,\ \text{no path}\ 1\to 4;\ H\ \text{is not a tree}

K=(\{7\},\varnothing)

K\ \text{is a tree},\ \text{leaves}(K)=\varnothing

Substeps and lemmas

\text{the set of lengths of walks}\ u\to v\ \text{is nonempty}

\exists\ \text{a walk}\ W\ \text{from}\ u\ \text{to}\ v\ \text{of least length}\ k

w_i=w_j\ (i<j)\ \text{in the least walk}\ W

\text{a walk of length}\ k-(j-i)<k,\ \text{contradiction; so}\ W\ \text{is a path}

C\ \text{simple cycle in}\ G-v

C\ \text{simple cycle in}\ G

C\ \text{simple cycle in}\ G,\ \deg_G(v)\le 1

v\notin C,\ C\ \text{simple cycle in}\ G-v

p_0=3\neq 6

p_1=2

p_1=2\neq 6

p_2=4

p_2=4\neq 6

p_3=6,\ m=3,\ P=(3,2,4,6)

Reverse audits

• S17 · premise_audit · G2, G3, mko_tree_def — It relies on two stated conventions: the zero-edge path is valid, and a leaf has degree exactly 1.
• S16 · premise_audit · G3, walk_path_cycle, mko_tree_def — Showing that a graph is not a tree requires only one failed condition; here two of them fail.
• S15 · premise_audit · S09, S12, S14, case_analysis — Uniqueness relies on G having no cycle (S09) and on the unique path (S12); cycles are identified when they differ only in starting point and direction, which the MKO handles by its fixed output convention.
• S14 · premise_audit · S11, S13, walk_path_cycle — Only existence is shown; uniqueness is in S15.
• S13 · premise_audit · G1, S10, graph_basics — If e were already in E, listing it again would create no new edge and the premise would fail (see the error controls).
• S12.3 · premise_audit · S12.2, S03, case_analysis — The two cases {5,6} exhaust all possibilities; the result is the path of S11.
• S12.2 · premise_audit · S12.1, S03, case_analysis — The two cases {1,4} exhaust all possibilities.
• S12.1 · premise_audit · S03, graph_basics — Only the neighbour list of 3 is used.
• S12 · premise_audit · S03, S11, walk_path_cycle, case_analysis — The exhaustion covers every neighbour at every stage, so it is a complete proof for this pair of vertices; it is not a proof of the general theorem.
• S11 · premise_audit · S03, walk_path_cycle, exists_intro — Only existence is shown; uniqueness is proved separately in S12.
• S10 · sufficient_goal_reduction · S02, S06, S09, mko_tree_def, and_intro_elim — Goal G: G is a tree. Sufficient condition H: the three conditions together; H⇒G by the definition. H is proved forwards in S02, S06 and S09, without using |E|=|V|−1 and without using G as a premise.
• S09 · premise_audit · S07, S08, logic_chain, walk_path_cycle — The conclusion relies on the whole chain of equivalences; if some deleted vertex had degree above 1 the chain would break, which is why S07 rechecks degrees each time.
• S08 · inverse_equivalence · L_leaf_cycle — The lemma is an equivalence, so the step is two-way.
• S07.2 · premise_audit · walk_path_cycle, graph_basics, contrapositive — The key is that k≥3 makes the two cycle neighbours distinct; with a 'cycle' (u,v,u) of length 2 the argument would fail, which is why the definition requires k≥3. The lemma itself is not used.
• S07.1 · premise_audit · delete_vertex, walk_path_cycle, subset_def — Only the inclusion of the subgraph is used; this direction needs no degree condition.
• S07 · inverse_equivalence · L_leaf_cycle, logic_chain — Each application of the lemma is an equivalence and equivalences chain, so the whole step is two-way; before each deletion the degree in the current graph is rechecked to be at most 1.
• S06.2 · premise_audit · S06.1, contradiction, walk_path_cycle — The contradiction rests only on the minimality of k and on the shortened sequence still being a walk; the lemma itself is not used.
• S06.1 · premise_audit · walk_path_cycle, well_ordering — Well-ordering needs nonemptiness, which the lemma's premise (a walk exists) supplies.
• S06 · premise_audit · S05, L_walk_path — Only 'vertex 1 reaches every vertex' and the lemma are needed; the 15 vertex pairs need not be listed one by one. Uniqueness of paths is not claimed.
• S05 · premise_audit · S03, walk_path_cycle, exists_intro — Each path only needs its edges and the no-repeat condition checked; this step does not claim the paths are unique.
• S04 · inverse_equivalence · S03, def_unfold — Both directions are checked point by point: each listed vertex has degree 1, and the unlisted 2 and 4 do not.
• S03 · premise_audit · S02, graph_basics, numeric_evaluation — Each edge {u,v} contributes v∈N(u) and u∈N(v) exactly once each; the matching handshake sum is an independent check of the neighbour lists.
• S02 · premise_audit · G1, graph_basics — This only checks the data format; no connectivity or acyclicity is claimed.
• S01 · premise_audit · G1, G2, mko_tree_def — This step only unfolds the definition and derives nothing new; the three conditions are proved separately later.

Error controls and negative controls

Edge count alone does not determine whether a graph is a tree

The misconception the MKO names: deciding that a graph is a tree from |E|=|V|−1 alone. H (a triangle plus the isolated vertex 4) has 4 vertices and 3 edges, yet is disconnected and has a cycle. This guide decides that G is a tree without using the edge count at all, by proving connectivity and acyclicity directly (S06, S09).

A single-vertex tree has no leaf

K=({7},∅) is a tree, but deg(7)=0, not 1, so under this MKO's leaf convention its leaf set is empty. Calling a degree-0 vertex a leaf is another misconception the MKO names.

An existing edge cannot be 'added' again

{2,4} is already in E; listing it again leaves the normalized edge set unchanged and creates no cycle. Treating (2,4,2) as a cycle fails the requirement k≥3 for a simple cycle. MKO assumption a3 requires the added edge to be absent from the original graph.

Write paths in vertex order

A path is a sequence, not a set. (3,2,4,6) differs from the sorted (2,3,4,6): the latter does not start at 3, and {3,4} is not an edge.

• H has 4 vertices and 3 edges, so H is a tree → reject — Vertex 4 is isolated, so H is disconnected; and (1,2,3,1) is a simple cycle.
• The vertex 7 of K=({7},∅) is a leaf → reject — deg(7)=0, while a leaf needs degree exactly 1.
• Adding {2,4} to G once more creates the cycle (2,4,2) → reject — {2,4} is already in E, so the edge set is unchanged; (2,4,2) has length 2<3 and is not a simple cycle.
• The path from 3 to 6 is (2,3,4,6) → reject — It does not start at 3, and {3,4}∉E; the correct path is (3,2,4,6).
• G+{3,6} has two different simple cycles, (3,2,4,6,3) and (6,4,2,3,6) → reject — The second is the same cycle with another starting point and the opposite direction; both have edge set {{3,2},{2,4},{4,6},{6,3}} (S15).

Result and limitations

G is a tree: V is nonempty, vertex 1 reaches every vertex so G is connected, and deleting leaves down to a single vertex shows there is no simple cycle. The leaves are {1,3,5,6}. The unique path from 3 to 6 is (3,2,4,6). After adding the new edge {3,6} there is exactly one simple cycle, (3,2,4,6,3). Contrast: H has |E|=|V|−1 but is disconnected and has a cycle, so it is not a tree; the single-vertex graph K is a tree with an empty leaf set.

• The general theorems 'any two vertices of a tree have a unique path' and 'a finite tree has |V|−1 edges' are not proved here; the uniqueness in S12 is proved by exhaustion for 3 and 6 only.
• Cycles are identified when they differ only in starting point and direction; the MKO removes this choice by a fixed output convention (start at the smaller label, follow the original path).

Verification and source binding

8 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 2705a4400701f09e6a4f469a879e803b4a263ba61ee3436c9788c3e7c6c938dc
• original source SHA-256: 2705a4400701f09e6a4f469a879e803b4a263ba61ee3436c9788c3e7c6c938dc
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)