Let $G$ be a (simple finite) edged-weighted undirected connected graph with at least two vertices. Let ST mean spanning tree and MST mean minimum spanning tree. Let me define some less common terms first.
- An edge is unique-cycle-heaviest if it is the unique heaviest edge in some cycle.
- An edge is non-cycle-heaviest if it is never a heaviest edge in any cycle.
- An edge is unique-cut-lightest if it is the unique lightest edge to cross some cut.
- An edge is non-cut-lightest if it is never a lightest edge to cross any cut.
- Two STs are adjacent if every ST has exactly one edge that is not in the other ST.
- An MST is an isolated MST if it is not adjacent to another MST (when both MSTs are considered as STs).
When are there more than one minimum spanning tree?
To answer OP's question, here are five characterizations of $G$ that has more than one MST.
- There are two adjacent MSTs.
- There is no isolated MST.
- There is an ST which is as light as or lighter than all adjacent STs and which is as light as one adjacent ST.
- There is an edge which is neither unique-cycle-heaviest nor non-cycle-heaviest.
- There is an edge which is neither unique-cut-lightest nor non-cut-lightest
The novelty of this answer is mostly the last two characterizations. The second from last characterization can be considered as the very next step of the OP's approach. The first three characterizations together can be considered as a slightly enhanced version of dtt's answer.
It is easier to think in the opposite term, whether $G$ has a unique MST. The following is the opposite and equivalent version of the above characterizations.
When is the minimum spanning trees unique?
Theorem: the following properties of $G$ are equivalent.
- Uniqueness of MST: There is a unique MST.
- No adjacent MST: there is no adjacent MSTs.
- One isolated MST: there is an isolated MST.
- One local minimum ST: there is an ST which is lighter than all adjacent STs.
- Extreme cycle edge: every edge is either unique-cycle-heaviest or non-cycle-heaviest.
- Extreme cut edge: every edge is either unique-cut-lightest or non-cut-lightest
Here comes my proof.
"Uniqueness of MST" => "No adjacent MST": obvious.
"No adjacent MSTs" => "One isolated MST": obvious.
"One isolated MST" => "One local minimum ST": An isolated MST is lighter than all adjacent STs.
"One local minimum ST" => "Extreme cycle edge": Let $m$ be an ST that is lighter than all adjacent STs.
- Every edge in $m$ must be non-cycle-heaviest. Here is the proof. Let $l$ be an edge in $m$. If $l$ does not belong to any cycle, we are done. Now suppose $l$ belongs to a cycle $c$. If we remove $l$ from $m$, $m$ will be split into two trees, which will be named $m_1$ and $m_2$. As a cycle that connects $m_1$ and $m_2$ with $l$, $c$ must have another edge that connects $m_1$ and $m_2$. Name that edge $l'$. Let $m'$ be the union of $m_1$, $m_2$ and $l'$, which must be a spanning tree of $G$ as well. Since $m$ and $m'$ are adjacent, $m$ is lighter than $m'$. That means, $l$ is lighter than $l'$. So $l$ is non-cycle-heaviest.
- Every edge not in $m$ must be unique-cycle-heaviest. Here is the proof. Let $h'$ be an edge not in $m$. If we add $h'$ to $m$, we will create a cycle $c$. Let $h$ be an edge in $c$ that is not $h'$. Consider the spanning tree $m'$ made from $m$ with $h$ replaced by $h'$. Since $m$ and $m'$ are adjacent, $m$ is lighter than $m'$. That means, $h$ is lighter than $h'$. So $h'$ is the unique heaviest edge in $c$. That is, $h'$ is unique-cycle-heaviest.
"Local minimum ST" => "Extreme cut edge": Proof is left as an exercise.
"Extreme cycle edge" => "Uniqueness of MST": Let $m$ be an MST. Let $e$ be an arbitrary edge. If $e$ is non-cycle-heaviest, $m$ must contain it. If edge $e$ is unique-cycle-heaviest, $m$ cannot contain it. (These two propositions can be proved by the standard reasoning about MST using cycle and edge exchange, similarly to what have been done just above). Hence $m$ is exactly the set of non-cycle-heaviest edges.
"Extreme cut edge" => "Uniqueness of MST": Proof is left as an exercise.
The above chains of implications proves the theorem.
Once again, the novelty of this answers is mostly the "extreme cycle edge" property and the "extreme cut edge" property, which uses the concepts, non-cycle-heaviest and non-cut-lightest. I have not seen those concepts elsewhere, although they are quite natural.
Here are two related interesting observations.
- For any edge $e$, $e$ is non-cycle-heaviest $\Leftrightarrow$ $e$ is unique-cut-lightest $\Leftrightarrow$ $e$ is in every MST
- For any edge $e$, $e$ is unique-cycle-heaviest $\Leftrightarrow$ $e$ is non-cut-lightest $\Leftrightarrow$ $e$ is not in any MST
Two sufficient but not necessary conditions for unique MST
the uniqueness of the heaviest edge in every cycle implies the "extreme cycle edge" property. So it is a sufficient condition. A counterexample to its being necessary condition is the graph with weights $ab\rightarrow 1, bc\rightarrow 1, cd\rightarrow 1, da\rightarrow 2, ac\rightarrow 2$.
the uniqueness of the lightest edge in every cut-set implies the "extreme cut edge" property. So it is a sufficient. A counterexample to its being necessary condition is a triangle with weights $1,1,2$.