A square Dris index forces $p\equiv k\equiv 1 \pmod{16}$ and $6\nmid k+1$

Proved

OddPerfectNumber.dris_square_index_exp_mod_sixteen

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

number-theory

Let $N = p^{k}m^{2}$ be an odd perfect number in Euler form, so that $p$ is prime with $p \equiv 1 \pmod 4$ , $k \equiv 1 \pmod 4$ , $m$ is odd, and the Dris relations

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

hold with index $s = \sigma(m^{2})/p^{k}$ . Suppose in addition that the index is a perfect square, $s = u^{2}$ . Then

p \equiv 1 \pmod{16}, \qquad k \equiv 1 \pmod{16}, \qquad 6 \nmid k+1 .

The point is that a square index collapses the first Dris relation to the classical equation " $\sigma(p^{k})$ is twice a square": the index is odd and divides $m^{2}$ , so $u \mid m$ and

\sigma(p^{k}) \;=\; 2\left(\frac{m}{u}\right)^{2}.

The two known constraints on that equation — the congruences $p \equiv k \equiv 1 \pmod{16}$ , and its insolubility when $6 \mid k+1$ — then apply verbatim.

Consequently no odd perfect number can have a square Dris index at a special exponent $k \not\equiv 1 \pmod{16}$ ; in particular not at $k = 5$ , $k = 9$ or $k = 13$ . This covers every index of the form $s = q^{2}$ with $q$ prime, the smallest composite case left open by the treatment of the indices $s = 1$ and $s$ an odd prime.

Preamble

import Mathlib

Formal statement

namespace OddPerfectNumber

theorem dris_square_index_exp_mod_sixteen (p k m s u : Nat)
    (hp : p.Prime) (hp4 : p % 4 = 1) (hk4 : k % 4 = 1) (hm : Odd m)
    (hsq : s = u ^ 2)
    (h1 : 2 * m ^ 2 = (∑ d ∈ (p ^ k).divisors, d) * s)
    (h2 : (∑ x ∈ (m ^ 2).divisors, x) = p ^ k * s) :
    p % 16 = 1 ∧ k % 16 = 1 ∧ (k + 1) % 6 ≠ 0 := 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); the constraints on sigma(p^k) = 2 w^2 are the platform theorems OddPerfectNumber.prime_and_exp_mod_sixteen_of_sigma_eq_two_mul_sq and OddPerfectNumber.sigma_prime_pow_ne_two_mul_sq_of_six_dvd.

View graph

A square Dris index forces p≡k≡1(mod16)p\equiv k\equiv 1 \pmod{16}p≡k≡1(mod16) and 6∤k+16\nmid k+16∤k+1

A square Dris index forces $p\equiv k\equiv 1 \pmod{16}$ and $6\nmid k+1$