Dris nine-case, odd s: non-square subcase
OpenOddPerfectNumber.no_dris_nine_s_ge_two_not_even_nonsqdivisor-functionnumber-theory
Non-square- remainder of the Dris , odd leaf: with not a square, the two Dris equations are still impossible. Needs order/modular analysis beyond the square case.
Preamble
import Mathlib.Tactic
Formal statement
namespace OddPerfectNumber theorem no_dris_nine_s_ge_two_not_even_nonsq (p k m s : Nat) (hp : p.Prime) (hp2 : p != 2) (hp4 : p % 4 = 1) (hk4 : k % 4 = 1) (hk9 : k = 9) (hm : Odd m) (hpm : ¬ p ∣ m) (hs2 : 2 ≤ s) (hs_not_even : ¬ Even s) (hs_nsq : ¬ ∃ r, s = r ^ 2) : ¬ (2 * m ^ 2 = (∑ d ∈ (p ^ k).divisors, d) * s ∧ (∑ d ∈ (m ^ 2).divisors, d) = p ^ k * s) := by sorry end OddPerfectNumber
Source