Although your question is vague in certain ways, one robust answer to it is provided by the subject known as Reverse Mathematics. The nature of this answer is different from what you had suggested or solicited, in that it is not based on any observed data of mathematical practice, but rather is based on the provable logical relations among the classical theorems of mathematics. Thus, it is a mathematical answer, rather than an engineering answer.
The project of Reverse Mathematics is to reverse the usual process of mathematics, by proving the axioms from the theorems, rather than the theorems from the axioms. Thus, one comes to know exactly which axioms are required for which theorems. These reversals have now been carried out for an enormous number of the classical theorems of mathematics, and a rich subject is developing. (Harvey Friedman and Steve Simpson among others are prominent researchers in this area.)
The main, perhaps surprising conclusion of the project of Reverse Mathematics is that it turns out that almost every theorem of classical mathematics is provably equivalent, over a very weak base theory, to one of five possibilities. That is, most of the theorems of classical mathematics turn out to be equivalent to each other in five large equivalence classes.
For example,
Provable in and equivalent to the theory RCA0 (and each other) are: basic properties of the natural/rational numbers, the Baire Cateogory theorem, the Intermediate Value theorem, the Banach-Steinhaus theorem, the existence of the algebraic closure of a countable field, etc. etc. etc.
Equivalent to WKL0 (and each other) are the Heine Borel theorem, the Brouer fixed-point theorem, the Hahn-Banach theorem, the Jordan curve theorem, the uniqueness of algebraic closures, etc. , etc. etc.
Equivalent to ACA0 (and each other) are the Bolzano-Weierstraus theorem, Ascoli's theorem, sequential completeness of the reals, existence of transcendental basis for countable fields, Konig's lemma, etc., etc.
Equivalent to ATR0 (and each other) are the comparability of countable well orderings, Ulm's theorem, Lusin's separation theorem, Determinacy for open sets, etc.
Equivalent to Π11 comprehension (and each other) are the Cantor-Bendixion theorem and the theorem that every Abelian group is the direct sum of a divisible group and a reduced group, etc.
The naturality and canonical nature of these five axiom systems is proved by the fact that they are equivalent to so many different classical theorems of mathematics. At the same time, these results prove that those theorems themselves are natural and essential in the sense of the title of your question.
The overall lesson of Reverse mathematics is the fact that there are not actually so many different theorems, in a strictly logical sense, since these theorems all turn out to be logically equivalent to each other in those five categories. In this sense, there are essentially only five theorems, and these are all essential. But their essential nature is mutable, in the sense that any of them could be replaced by any other within the same class.
I take this as a robust answer to the question that you asked (and perhaps it fulfills your remark that you thought ideally the answer would come from proof theory). The essential nature of those five classes of theorems is not proved by looking at their citation statistics in the google page-rank style, however, but by considering their logical structure and the fact that they are logically equivalent to each other over a very weak base theory.
Finally, let me say that of course, the Reverse Mathematicians have by now discovered various exceptions to the five classes, and it is now no longer fully true to say that ALL of the known reversals fit so neatly into those categories. The exceptional theorems are often very interesting cases which do not fit into the otherwise canonical categories.
Best Answer
HoTT/HoTT Categories
Links: https://github.com/HoTT/HoTT/tree/master/theories/Categories (current), https://github.com/JasonGross/HoTT-categories (old), https://bitbucket.org/JasonGross/catdb (oldest). Interactive index, non-interactive index, top-level wiki
Language: Coq 8.6; will compile with 8.7 when it comes out; the oldest version compiled with Coq 8.4)
Author: Jason Gross
Active Development: No, but actively maintained in its present form (as of June 2017)
Concepts Formalized:
1-precategories (in the sense of the HoTT Book)
univalent/saturated categories (or just categories, in the HoTT Book)
functor precategories $\mathcal C \to \mathcal D$
dual functor isomorphisms $\text{Cat} \to \text{Cat}$; and $(\mathcal{C} \to \mathcal{D})^{\text{op}} \to (\mathcal{C}^{\text{op}} \to \mathcal{D}^{\text{op}})$
the category Prop of ($U$-small) hProps
the category Set of ($U$-small) hSets
the category Cat of ($U$-small) strict (pre)categories (strict in the sense of the objects being hSets)
pseudofunctors
profunctors
adjoints
Yoneda lemma
Exponential laws
Concepts currently under construction:
Construction Choices: