What is an efficient nesting of mathematical theorems?
Solution 1:
The premise of this question, which seems to be that there a key general theorems in mathematics from which other results can be deduced, is a little dubious. (There are also some inaccuracies in the post: e.g. Grothendieck--Hirzebruch--Riemann--Roch is a theorem in algebraic geometry, not category theory.)
Let me discuss just one fundmental theorem: the prime number theorem. On the one hand, this fits into a whole family of related theorems, all of fundamental significance in number theory: the asymptotic form of Dirichlet's theorem on primes in arithmetic progression; Cebotarev's density theorem; or, more recently, the Sato--Tate conjecture. On the other hand, there is no general result from which these results all follow.
More precisely, all these results can be proved by showing that an appropriate $L$-function (or family of $L$-functions) has analytic continuation up to the line $\Re(s) \geq 1$, and has no zeroes in this region. Given this, the claimed result then follows from the Wiener--Ikehara Tauberian theorem; so this is a general result which is involved in their proof. And this result can be realized as a special case of the much more general result in the theory of $L^1$ of locally compact groups, due to Gelfand. So that very general Tauberian theorem could feature as one vertex on the proposed network.
But this leaves open the question of how to affect the analytic continuation on $\Re(s) \geq 1$ (and how to verify the zero-freeness there). There is no general theorem that implies this. There are very general conjectures, in particular those coming from the Langlands program(see also the various posts on the Langlands program linked to here for more information on this program). But these are conjectures, not general theorems (as of yet).
There has been enormous progress on this program: e.g. Taylor and Wiles's proof of Shimura--Taniyama, or Sato--Tate, or Ngo's Fields Medal-winning work on the fundamental lemma. But these result reach out from what is known into the unknown. They involve an enormous amount of mathematics, including many results that would appear on the vertices of the envisaged network (algebraic geometry and etale cohomology, perverse sheaves, class field theory, ...). But all evidence suggests that it will be a long time before the general statement that encompases them all (the general form of Langlands's functoriality and reciprocity conjectures) is proved.
The conclusion that I draw from this is that, to the extent that mathematics is a living subject, it reaches out into the unknown; and the underlying principles are always being reformulated, with new ones being discovered. (As just one example of a recently discovered fundamental framework that is related to the prime number theorm, but is not part of the Langlands program, see the use of nilsystems in the work of Green and Tao on linear equations in primes.) In short, the envisaged network doesn't exist, at least as a way to encompass mathematics as a continually evolving subject. (Incidentally, I would also object to such a framework from a pedagogical view-point, but that is a different topic.)
Solution 2:
At the end of the day it sounds like you want a directed graph with a node for every provable assertion and directed arcs representing logical implication.
In order for such a graph to be most useful you would ideally need to find a "normal form" for each provable assertion (or node).
But I don't see how this is possible, even restricting attention to assertions written in an extremely limited "sublanguage" of mathematics - consider "classical" Euclidean geometry, for example, where even a single theorem can typically find expression in several different equally valid, abstract, elegant, etc. forms (completely visual "proofs" of the Pythagorean theorem come to mind).
I suspect the best you can do is add "less than perfectly general" arcs and nodes to your logical graph via explicit proofs (written and read by humans). You could then have an automaton traverse the graph to find "cycles" (which indicate a set of "logically equivalent" assertions), "sources" (which indicate powerful statements), and "sinks" (which indicate weak ones).
But the usefulness of such a graph (even if received in Complete Perfection by a Supreme Intelligence) is limited by our ability to find the node for a given logical assertion. Making the statements as abstract as possible reduces the number of nodes in the graph (which may help) but may make it harder to decide if a given node (e.g. a theorem in Category Theory) really is equivalent to (or stronger than) the particular assertion we're interested in (e.g. a theorem in algebraic topology).
But maybe we're in a better position today to make the "search" for relevant nodes easier (e.g. by decorating the abstract statement of a theorem with "links" to equivalent forms and specific applications) than were previous generations of logicians. And if you actually start to build the graph maybe you'll figure out a format for "nodes" and "edges" that is sufficiently general to make the project appealing to other people, and you can make some progress.
Good luck!
EDIT: The distinction between "nodes" and "edges" is of course artificial - after all, logical statements boil down to implication, e.g. "A and B together imply C", and "logical statement X is stronger than logical statement Y" is itself a logical statement. But since the question seems to be about exploring relationships between logical statements I think it makes sense to distinguish the statements themselves (nodes) and logical relationships between them (arcs).
Solution 3:
A classical theorem
On the frontiers of math I can not say anything. I think I share the pursuit of what I'll call "general theorems" or "fundamental theorems". But if you can let me give an example of a "general theorem" in classical analysis. This theorem gives conditions for the two repeated limits commute. This theorem is widely does not receive due attention.
This theorem can be found in books of Lang (Analysis vol. 2 for example). But I think the wording of Zorich (Mathematical Analysis II p. 381) more generally. I will state it as it is in Zorich that describes in detail all the above mentioned consequences of this theorem. It's a pity we can not visualize them in google.
Theorem. Let $\{ F_t ; t\in T\}$ be a family of functions $F_t : X \rightarrow \mathbb{C}$ depending on a parameter t; let $\mathcal{B}_X$ be a base $X$ and $\mathcal{B}_{T}$ a base in $T$. If the family converges uniformly on $X$ over the base $\mathcal{B}_{T}$ to a function $F : X \rightarrow \mathbb{C}$ and the limit $\lim_{\mathcal{B}_{T}} F_t(x)=A_t$ exists for each $t\in T$, the both repeated limits $\lim_{\mathcal{B}_{X}}(\lim_{\mathcal{B}_{T}}F_t(x))$ and $\lim_{\mathcal{B}_{T}}(\lim_{\mathcal{B}_{X}}F_t(x))$ exist and the equality
$$ \lim_{\mathcal{B}_{X}}(\lim_{\mathcal{B}_{T}}F_t(x))=\lim_{\mathcal{B}_{T}}(\lim_{\mathcal{B}_{X}}F_t(x)) $$ holds.
The uniform convergence required in the hypotheses of this theorem is obtained via compactness and monotonicity when possible way (for example if $X = \mathbb{R}$).
For a convenient definition of the set $T$ (usually $T = \mathbb{N},\mathbb{R}$) and of functions $F_t$ (whit $X=\mathbb{R},\mathbb{R}^n,\mathbb{N}$ for exemple) follows immediately the following theorems
1) classical Fubini's theorem
2) Leibniz's rule for differentiation under the integral sign
3) Schwarz's theorem
4) Fundamental Calculu´s theorem
5) Arzelà–Ascoli theorem ( local version )
6) differentiation on the limit of some parameter
7) integration on the limit of some parameter
(Note. I hope I have written in English language common names of these theorems above.)
I'm not sure about that but I would venture to put on the list above theorems for continuous and differentiable dependence to ode and also the classical theorem of Weierstrass approximation.
I hope I have contributed to this example.
Solution 4:
Philosophy is the hierarchical organization of ideas, and what you are asking for is tantamount to a philosophy of mathematics. This will depend on what you consider meaningful, important, and interesting. Every age (in German, Zeitgeist) is going to have their own answer to this question, which defines that age. And every individual likewise has their own perspective, which stands in relation to that. If you read the preface of an outstanding math book, and if the author is able to express their experience, you will also gain much insight to lead you closer to your personal answer to this question.