No Dris-index solution for the Euler equation with special exponent and
OpenOddPerfectNumber.no_dris_special_exponent_five_s_ge_twodiophantine-equationsdivisor-sumsnumber-theoryperfect-numbers
Let be an odd prime with , let be odd with , and let be a natural number. The Euler equation for an odd perfect number in Euler form with special exponent has no Dris-index solution: the two relations and cannot both hold. This is the nontrivial case left after the case is ruled out by the proved lemma since .
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber
theorem no_dris_special_exponent_five_s_ge_two (p m s : ℕ) (hp : p.Prime) (hp2 : p ≠ 2)
(hp4 : p % 4 = 1) (hm : Odd m) (hpm : ¬ p ∣ m) (hs : 2 ≤ s) :
¬ (2 * m ^ 2 = (∑ d ∈ (p ^ 5).divisors, d) * s ∧
(∑ d ∈ (m ^ 2).divisors, d) = p ^ 5 * s) := by
sorry
end OddPerfectNumberSource
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 (Dris parametrisation of the Euler equation); Euler form and special-exponent case k = 5 as recorded on the Odd Perfect Number Conjecture mission.