Dris five-case, odd non-square $s$ : with a prime $\ell\ne3$ of $p^4+p^2+1$ dividing $s$ to an odd power

Open

OddPerfectNumber.no_dris_five_s_ge_two_not_even_nonsq_odd_val_prime

by vebis · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

divisor-functionnumber-theory

This is the non-square-index subcase of the Dris $k=5$ , $s\ge 2$ odd leaf (no_dris_five_s_ge_two_not_even_nonsq), with one additional hypothesis: the index $s$ is divisible to an odd power by some prime $\ell\ne 3$ dividing $p^4+p^2+1$ . For $p$ an odd prime, $m$ odd with $p\nmid m$ , and $s\ge 2$ odd and not a perfect square, the pair of relations

2m^{2}=\sigma(p^{5})\,s,\qquad \sigma(m^{2})=p^{5}s

is impossible.

The extra hypothesis is not a genuine restriction of the original leaf: by OddPerfectNumber.five_dris_index_odd_valuation_prime it follows from the first relation alone. It records, for anyone attacking the leaf, that $s$ always carries an odd power of a prime $\ell\equiv 1\pmod 6$ dividing $p^4+p^2+1$ , in particular $s\ge 7$ and $s$ is not a power of $3$ .

Formalization Note The conclusion is stated exactly as in the parent leaf, as $\neg(\text{both relations})$ .

Preamble

import Mathlib

Formal statement

namespace OddPerfectNumber

theorem no_dris_five_s_ge_two_not_even_nonsq_odd_val_prime (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_nsq : ¬ ∃ r, s = r ^ 2)
    (hl : ∃ ℓ : Nat, ℓ.Prime ∧ ℓ ≠ 3 ∧ ℓ ∣ p ^ 4 + p ^ 2 + 1 ∧ Odd (padicValNat ℓ s)) :
    ¬ (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

Dris five-case, odd non-square sss: with a prime ℓ≠3\ell\ne3ℓ=3 of p4+p2+1p^4+p^2+1p4+p2+1 dividing sss to an odd power

Dris five-case, odd non-square $s$ : with a prime $\ell\ne3$ of $p^4+p^2+1$ dividing $s$ to an odd power