Nielsen Theorem 1: $N < (d+1)^{4^k}$ for odd $n/d$-perfect $N$

This is Theorem 1 of Nielsen 2003 (pages 4-7), the general upper bound from which the odd-perfect milestone follows.

Let $N$ be odd and $n/d$-perfect with $n, d$ positive, i.e. $\sigma(N)\,d = n\,N$ where $\sigma$ is the sum-of-divisors function, and let $k$ be the number of distinct prime divisors of $N$. Then

The published proof strengthens Heath-Brown's algorithm: starting from any prime set $S$, Cases 1-2 build a disjoint extension $S'$ giving inequalities (1)-(2), then a subset $S'' \subseteq S \cup S'$ giving (3)-(4); a long calculation yields the key estimate (5), which replaces inequality (iv) of Heath-Brown's Lemma 2. The Heath-Brown induction (p. 196) with (5) in place of (iv) gives the bound. The odd-perfect corollary ($n = 2$, $d = 1$) is $N < 2^{4^{k}}$.

Formalization Note The $n/d$-perfect hypothesis is stated cross-multiplied in $\mathbb{N}$ as ArithmeticFunction.sigma 1 N * d = n * N, and $k$ is N.primeFactors.card.