Prime-chain lower bound for local length (source code)

= Prime-chain lower bound for local length
{title2=$H_R(t)\geq c\,t^s$}

A <prime chain> of length $s$ in a <Noetherian local ring> forces its maximal-<ideal> length function to be at least $ct^s$ for large $t$. Quotient by the initial prime to reduce to a domain, choose a nonzero $a$ in the next prime, and use the <Artin-Rees lemma> to obtain $H_R(t)\geq H_R(t-c_0)+H_{R/(a)}(t)$. Induction on chain length and summing about $t/(2c_0)$ terms prove the bound. This yields $\dim R\leq d(R)$ without assuming the <Krull height theorem>.