I am looking for a proof of a particular theorem. The theorem would state:
Every finite, weakly connected digraph contains at least one source or cycle.
Since every finite graph is either cyclic or acyclic, an alternative statement would be:
Every finite, weakly connected, acyclic digraph has a source.
with the previous theorem as a corollary.
Note: Assuming that the above is correct, then for any natural number $n$, an effective procedure exists to show that every weakly connected, acyclic digraph with fewer than $n$ vertices has a source - namely, "pick a point and backtrack". While this makes the theorem seem trivial, it is insufficient to prove that every finite, weakly connected, acyclic digraph has a source, hence the request for a proof.
I checked the library, all of my textbooks, and searched online, but I can't seem to find any reference to this theorem. The notion seems sufficiently obvious so as to be a fundamental result in graph theory, but no one I've spoken to has been able to put a name to it.
Is there a name for this theorem (or other, more significant theorem from which it can be easily derived), and where can I find a proof of it?
I don't know of a particular name for the theorem, but the idea of "pick a point and backtrack" is pretty much a proof - you can formalize it as follows, by proving the contrapositive:
Then to prove it, let $n$ be the number of vertices and let $x_0$ be an arbitrary vertex. Choose a sequence $x_1,\ldots,x_n$ with the property that $x_i$ has an edge to $x_{i-1}$. This is possible since there are no sources. However, now we have a sequence $x_0,\ldots,x_n$ with $n+1$ elements, thus by the pigeonhole principle, some pair must be the same - that is $x_i=x_j$ for some $j\neq i$. Assume without loss of generality that $i>j$. Then $$x_i\rightarrow x_{i-1} \rightarrow \ldots \rightarrow x_{j+1} \rightarrow x_j$$ is a cycle*.
(*If you insist upon a simple cycle, you can choose the a $(i,j)$ with $x_i=x_j$ and $i\neq j$ that minimizes $|i-j|$, since we know that the set of such pairs is non-empty)