The square-free part of the k=5 Dris index has at least two distinct prime factors
DisprovedOddPerfectNumber.Kernel.five_kernel_card_ge_twoLet be an odd perfect number with , and let be its Dris index, so for the Euler prime and the cofactor . Suppose the square-free part of is written as with square-free and is not itself a square. Then the square-free part has at least two distinct prime factors: .
The argument is short once the two exclusions are in place. If then is a square, contradicting the hypothesis; that is the accepted child OddPerfectNumber.Kernel.sqfree_part_ne_one (b59073fb). If is a prime then is exactly a prime times a square, which the accepted child OddPerfectNumber.Kernel.five_index_not_prime_mul_square (2ec27119) forbids, since it uses only the first Dris equation together with the factorisation and the coprimality and non-square properties of the two cyclotomic blocks. The accepted generic lemma OddPerfectNumber.Kernel.squarefree_card_ge_two_of_not_one_or_prime (9c90129e) then converts the two exclusions into the bound of two.
This is the half of the target for the Dris branch of OddPerfectNumber.no_dris_five_s_odd_ge_five_nonsq. The remaining half is the genuine research residual: excluding for two distinct primes, which the two-prime case genuinely satisfies as far as the first Dris equation alone is concerned (at , , one has exactly ), so the second Dris equation is indispensable there.
import Mathlib
namespace OddPerfectNumber.Kernel
theorem five_kernel_card_ge_two (p m s d1 d2 : Nat) (hp : p.Prime) (hp2 : p != 2)
(hp4 : p % 4 = 1) (hm : Odd m) (hpm : ¬ p ∣ m) (hs_nsq : ¬ ∃ r : Nat, s = r ^ 2)
(hd2 : d1 ^ 2 * d2 = s) (hd2pos : 0 < d2) (hdsf : Squarefree d2) :
2 ≤ d2.primeFactors.card := by
sorry
end OddPerfectNumber.Kernel