Unsure why (or whether?) a certain algorithm correctly computes a Minimum spanning tree

Question

CLRS problem 23-4 part c gives an algorithm that may or may not compute a minimum spanning tree. Given some connected undirected graph G, we have

MAYBE-MST-C(G,w)
  T = empty set
  for each edge e in G, taken in arbitrary order
    T = T U {e}
    if T has a cycle c
      let e' be a maximum-weight edge on c
      T = T - {e'}
  return T

I've found several other solutions (here, here and here) that claim that this procedure succeeds in finding an MST. However, I don't understand any of their proofs.

I can see that this results in a spanning tree. It's spanning because adding every edge e would certainly span G, and removing parts of cycles e' certainly doesn't affect that. It's a tree because any cycle that is added is guaranteed to be immediately removed.

I'm having a hard time seeing why it's minimal (or perhaps it actually isn't?). One of the solutions uses the result of exercise 23.1-5:

if $G$ and has some cycle $c$, then there exists some MST of G that does not include the edge $e'$ with the largest weight on that cycle $c$.

While this result superficially resembles the operation performed in MAYBE-MST-C, upon closer inspection, it's not so obvious that it helps, since in the algorithm, T is not guaranteed to span G until the very end, and also the exercise result only claims that an MST exists when omitting one e'; it doesn't say we need to remove all e'. What if the MST that the exercise guarantees requires us to remove the first e', but keep the second? Further, upon removing e', how are we sure that the edges needed to compete the MST have not been removed in previous iterations of the loop?

Answer 1

MAYBE-MST-C does obtain the minimum spanning tree correctly.

Define a "local MST" as a spanning tree for which any cycle resulting from adding some edge $e$ would not have any edges on the cycle with weight $> w(e)$.

Lemma: The tree $T$ generated by MAYBE-MST-C is a local MST.

Proof:

any edge $e$ that is not already in $T$ at the end of the algorithm must have been removed, and thus it must have been a part of some cycle $c$, and was a maximal-weight edge on that cycle at the time $e$ was removed.

Note the rest of $c - {e}$ could have been deformed after $e$ was removed, but each deformation can only replace an edge $f$ with a longer path consisting of weights that are at most $w(f) \leq w(e)$. Hence, if $e$ were added back into $T$ at the very end and completed some cycle $c'$ that had the final result of all those deformations, $e$ is still guaranteed to be a maximal-weight edge on $c'$.

Main result: MAYBE-MST-C results in a minimal spanning tree.

proof: From the lemma, MAYBE-MST-C results in a local MST, and since local MSTs are minimum, the result immediately follows.