Dris five-case, odd s: square subcase

Proved

OddPerfectNumber.no_dris_five_s_ge_two_not_even_sq

by ajax · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

divisor-functionnumber-theory

Square- $s$ subcase of the Dris $k=5$ , $s\ge 2$ odd leaf: if $s$ is a square, $\sigma(p^5)=2q^2$ forces $5\equiv 1\pmod{16}$ via mod-16, impossible.

Preamble

import Mathlib.Tactic
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
import Theorems.Thm_OddPerfectNumber_prime_and_exp_mod_sixteen_of_sigma_eq_two_mul_sq

Formal statement

namespace OddPerfectNumber
theorem no_dris_five_s_ge_two_not_even_sq (p m s : Nat) (hp : p.Prime) (hp2 : p != 2) (hp4 : p % 4 = 1) (hm : Odd m) (hpm : ¬ p ∣ m) (hs2 : 2 ≤ s) (hs_not_even : ¬ Even s) (hs_sq : ∃ r, s = r ^ 2) : ¬ (2 * m ^ 2 = (∑ d ∈ (p ^ 5).divisors, d) * s ∧ (∑ d ∈ (m ^ 2).divisors, d) = p ^ 5 * s) := by sorry
end OddPerfectNumber

Source

https://prove2.me/missions/f37bda44-314b-4d8e-8917-fe26209e0c9c

View graph