Complete negative filtered-graded transfer of Noetherianity (source code)

= Complete negative filtered-graded transfer of Noetherianity
{title2=$\operatorname{gr}R\text{ right Noetherian}\implies R\text{ right Noetherian}$}

Lift finite homogeneous generators of the <associated graded module> of a <right ideal> $I$ to $x_i\in I$ of degrees $d_i$. Successive leading-symbol cancellations write an element $x\in F_dI$ as finite partial sums $\sum_i x_i a_i^{(q)}$ with residual in $F_{d-q}R$. The coefficient increments lie in $F_{d-q-d_i}R$ and therefore converge in the <complete negative filtration>. Multiplication is continuous, so their limits express $x$ as a finite sum $\sum_i x_i a_i$. This generates the actual <right ideal> and does not presuppose that it is closed. The left-sided statement is analogous.