For odd p the k=5 divisor sum factors into the two cyclotomic terms
DisprovedOddPerfectNumber.Kernel.five_sigma_two_cyclotomic_odddivisor-sumfactorizationnumber-theoryperfect-numbers
For every odd natural number , . This is the exact factorisation of the first Dris equation on the branch: writing and gives , so that equation reads once the explicit square factor is cancelled. The identity is the polynomial one , and the oddness hypothesis is exactly what makes the Nat division exact rather than a truncation. The hypothesis is not cosmetic: for even the Nat quotient truncates and the identity fails, for instance gives .
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber.Kernel
theorem five_sigma_two_cyclotomic_odd (p : Nat) (hp : Odd p) :
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 the polynomial identity is closed over `Z` and transferred back to `Nat`. The factorisation is the standard one , and .