For k=5 the Dris index equation factors into the two cyclotomic terms
DisprovedOddPerfectNumber.Kernel.five_sigma_two_cyclotomicdivisor-sumfactorizationnumber-theoryperfect-numbers
For every natural number , . This is the exact factorisation of the first Dris equation on the branch: writing and gives , so that equation reads once is cancelled. The identity is a polynomial one, since ; no oddness assumption on is required, and the division by is exact for every because .
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber.Kernel
theorem five_sigma_two_cyclotomic (p : Nat) :
2 * (p ^ 2 + p + 1) * (((p + 1) / 2) * (p ^ 2 - p + 1)) =
∑ d ∈ (p ^ 5).divisors, d := by
sorry
end OddPerfectNumber.KernelSource
Mathlib/NumberTheory/Divisors.lean (`sum_divisors_prime_pow`, the additive form of `prod_divisors_prime_pow` at line 516) rewrites the divisor sum over .divisors as a sum over `range 6`, after which `ring` proves the polynomial identity. The factorisation is the standard one .