No odd perfect number whose Dris index is an odd prime, when has at most one odd prime factor
ProvedOddPerfectNumber.no_dris_index_odd_prime_of_one_odd_primeA prime Dris index is impossible when has at most one odd prime factor.
In the Dris parametrisation of a hypothetical odd perfect number (Euler form: the special prime, odd, ), the index is the number with
This statement rules out every odd prime index , for every special exponent whose successor has at most one odd prime divisor, i.e. with prime. In particular it settles the indices for the special exponents , where . (The index of an odd perfect number is always odd, since is odd for odd ; the case is the theorem of Dandapat–Hunsucker–Pomerance.)
The hypothesis on is formalized as , and is written as the sum over the divisor finset.
The proof rests on a counting bound for the prime support of . Because is prime, has only two prime divisors. For a prime with and , the divisor sum divides ; if it is a pure power of , then a lifting-the-exponent argument in the style of Dandapat–Hunsucker–Pomerance forces , and otherwise , which by can happen for at most one prime . Hence the primes of lie among , the odd prime dividing , and one exceptional prime, so — contradicting Sylvester's bound for odd perfect numbers.
import Mathlib
namespace OddPerfectNumber
theorem no_dris_index_odd_prime_of_one_odd_prime (p k m s : Nat)
(hp : p.Prime) (hs : s.Prime) (hs2 : s ≠ 2) (hk : k ≠ 0) (hm : Odd m) (hpm : ¬ p ∣ m)
(hk1 : ((k + 1).primeFactors.erase 2).card ≤ 1) :
¬ (2 * m ^ 2 = (∑ d ∈ (p ^ k).divisors, d) * s ∧
(∑ d ∈ (m ^ 2).divisors, d) = p ^ k * s) := by
sorry
end OddPerfectNumber