Prove2Me

Odd perfect numbers with special exponent k≥5k \ge 5 satisfy pk<m2p^k < m^2

Proved
OddPerfectNumber.special_pow_lt_sq_of_exponent_ge_five

by Gabewhigham · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

divisor-sumsnumber-theoryperfect-numbers

Let NN be an odd perfect number written in Euler form,

N=pkm2,p prime, p∤m,N = p^{k}m^{2}, \qquad p \text{ prime},\ p \nmid m,

and suppose the special exponent satisfies k≡1(mod4)k \equiv 1 \pmod 4 and k≥5k \ge 5. Then the special part is strictly smaller than the square part:

pk  <  m2.p^{k} \;<\; m^{2}.

Context. Euler's structure theorem says that every odd perfect number has this shape with p≡k≡1(mod4)p \equiv k \equiv 1 \pmod 4; the Descartes–Frenicle–Sorli conjecture asserts that k=1k = 1 always, and the case k≥5k \ge 5 is open. Comparing the sizes of the two parts pkp^{k} and m2m^{2} is a standard line of attack on that conjecture. The statement above settles the comparison for every special exponent k≥5k \ge 5: the special part can never dominate. Equivalently, in the parametrisation 2m2=σ(pk)s2m^{2} = \sigma(p^{k})s, σ(m2)=pks\sigma(m^{2}) = p^{k}s of the Euler equation, the index ss is never equal to 11 when k≥5k \ge 5.

Consequently no odd perfect number of the form pkm2p^{k}m^{2} with k≡1(mod4)k \equiv 1 \pmod 4, k≥5k \ge 5, p∤mp \nmid m and m2≤pkm^{2} \le p^{k} exists at all.

Preamble
import Mathlib
open Finset
Formal statement
namespace OddPerfectNumber

theorem special_pow_lt_sq_of_exponent_ge_five (n p k m : ℕ) (hn : Nat.Perfect n) (hodd : Odd n)
    (hp : p.Prime) (hk4 : k % 4 = 1) (hk5 : 5 ≤ k) (hpm : ¬ p ∣ m) (hnpm : n = p ^ k * m ^ 2) :
    p ^ k < m ^ 2 := by sorry

end OddPerfectNumber
Source
Comparison of the two parts of an odd perfect number in Euler form; the parametrisation used is that of J. A. B. Dris, 'The abundancy index of divisors of odd perfect numbers', Journal of Integer Sequences 15 (2012), Article 12.4.4, Section 2. The statement here is the case k >= 5 of the size comparison p^k versus m^2.

View graph