Special exponent $k=1$ : the Dris index has $\Omega(s) \ge 3$

Proved

OddPerfectNumber.dris_index_bigOmega_ge_three_at_k_one

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

number-theory

Consider an odd perfect number written in Euler form with special exponent $k = 1$ , that is, $N = p\,m^{2}$ with $p$ prime, $m$ odd and $p \nmid m$ — the configuration predicted by the Descartes–Frenicle–Sorli conjecture. The Dris relations then read

2m^{2} = \sigma(p)\,s, \qquad \sigma(m^{2}) = p\,s,

with Dris index $s = \sigma(m^{2})/p$ . The assertion is that such an index cannot be too simple:

\Omega(s) \ \ge\ 3,

where $\Omega$ counts prime factors with multiplicity (in Lean, the length of s.primeFactorsList). In particular $s$ is neither $1$ , nor a prime, nor a product of two primes, so $s \ge 27$ .

The reason is a counting one. Since $\sigma(m^{2}) = p\,s$ has $p$ -adic valuation $1$ , at most one of the local divisor sums $\sigma(q^{2v_q(m)})$ , $q \mid m$ , can be divisible by $p$ ; every other local divisor sum is a factor $> 1$ of $s$ , and these factors are pairwise coprime. Hence $\omega(m) \le 1 + \Omega(s)$ . Sylvester's bound $\omega(N) \ge 5$ gives $\omega(m) \ge 4$ , and the claim follows.

No congruence conditions on $p$ or on $m$ beyond oddness are needed.

Preamble

import Mathlib

Formal statement

namespace OddPerfectNumber

theorem dris_index_bigOmega_ge_three_at_k_one (p m s : Nat)
    (hp : p.Prime) (hm : Odd m) (hpm : ¬ p ∣ m)
    (h1 : 2 * m ^ 2 = (∑ d ∈ p.divisors, d) * s)
    (h2 : (∑ x ∈ (m ^ 2).divisors, x) = p * s) :
    3 ≤ s.primeFactorsList.length := by
  sorry

end OddPerfectNumber

Source

J. A. B. Dris, The abundancy index of divisors of odd perfect numbers, Journal of Integer Seq. 15 (2012), Article 12.4.4, Section 2 (Dris parametrisation, index s = sigma(m^2)/p^k); J. J. Sylvester (1888) for omega(N) >= 5.

View graph

Special exponent k=1k=1k=1: the Dris index has Ω(s)≥3\Omega(s) \ge 3Ω(s)≥3

Special exponent $k=1$ : the Dris index has $\Omega(s) \ge 3$