Some data regarding the dependency graph of the stacks project (on April 18, 2012).
We think of the bottom of the graph (height 0) as the vertices whose tags correspond to results whose proofs do not refer to any other result. Height 1 is those which refer to a result of height 0. Etc. The maximum height is 78 which is attained by 06RD. The next few are
Height 77 : 06RA 06RF 07BE
Height 76 : 06QK 06R9 06RC 06UF 06UG 07BA
Height 75 : 06QI 06QJ 06UD 06UE 06UI 07B4 07B9
Height 74 : 06MF 06N3 06QH 07B3
Height 73 : 06G3 06QG 077A 0783 07AQ 07B8 07BC
Height 72 : 06MX 06PL 0771
Height 71 : 06MT 06PK 0765 0782 07AP
Height 70 : 06MR 06PJ 075Z 0770 0775
Height 69 : 050B 06FI 076Z 0785
The distribution (number of tags per height for height > 0) looks like this
Why do you think the histogram isn’t strictly decreasing? Also: it would be interesting to see the histogram broken out by which things are called Lemmas, which Propositions, and which Theorems; does the nomenclature match our intuitive understanding of those words, in which Lemmas have fewer precursors?
OK, I think the reason for the second low value is that much of the later parts of the stacks project depend on the main result of the bootstrap chapter (Tag 04S6) which occurs at height 60. I am not sure why there is the earlier dip. It may just be because many of the algebra results come earlier and many of the results on schemes depend on quite a few algebra/sheaf theory etc results so their height is at least 30.
There are way to many lemmas in the stacks project. I would love some help with a better way to name the lemmas, propositions, theorem, etc.