We ask when adding hidden layers improves generalization, in a model that keeps the layers fixed and varies only their number. A hidden layer is a self-map of a state space, a depth-k network composes at most k hidden layers with an output layer, and depth is compared within the nested family H₀⊂ H₁⊂⋯ built from one class F of hidden layers; this compares a deep network with shallower networks built from the same layers, not with wider ones. Our message is that the statistical cost of depth is the metric entropy of the set B(k,F) of compositions. The estimation error is bounded by an entropy integral over B(k,F) with constants that do not depend on the depth, and the bound is matched from below when the output layer can see the hidden states. For Lipschitz layers on a bounded state space this entropy grows at most polynomially in k, and it stays bounded, or grows only like log k, under contraction, equicontinuity, or nilpotent structure. Balanced against the approximation error, this gives depths k^∗(n) that grow with the sample size, and it separates the models whose estimation error is independent of the depth from those whose estimation error grows with it. Deep ReLU networks, unrolled solvers, and chain-of-thought computation are worked out; for the last two the number of steps is derived rather than assumed. All statements are machine-checked in Lean 4; the formalization and its blueprint are available at https://shosonoda.github.io/lean-deepgen/ .