In the k=5 Dris situation the Euler prime p has a nontrivial source in sigma(m^2)
ProvedOddPerfectNumber.Kernel.five_index_p_source_not_pfactorizationnumber-theoryperfect-numbers
Let p be a prime, m a natural number with m squared nonzero, and k at least 1. If p to the k divides the divisor sum of m squared, then some prime q dividing m squared satisfies p divides the sum of the first factorization-exponent-plus-one powers of q, and q can be taken to be different from p when p does not divide m.
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber.Kernel
theorem five_index_p_source_not_p (p k m : Nat) (hp : p.Prime) (hk : 1 ≤ k)
(hm2 : m ^ 2 != 0) (hpm : Not (Dvd.dvd p m))
(hdvd : Dvd.dvd (p ^ k) (∑ x ∈ (m ^ 2).divisors, x)) :
exists q : Nat, Dvd.dvd q (m ^ 2) /\ Not (Dvd.dvd p q) /\
Dvd.dvd p (∑ i ∈ Finset.range ((m ^ 2).factorization q + 1), q ^ i) := by
sorry
end OddPerfectNumber.Kernel