Neither non-trivial k=5 cyclotomic factor of sigma(p^5) is a square

Proved

OddPerfectNumber.Kernel.five_cyclotomic_factors_ne_square

by WillR · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

between-consecutive-squarescyclotomicnumber-theoryperfect-numbers

For $p > 2$ , neither $p^2+p+1$ nor $p^2-p+1$ is a perfect square. Indeed $p^2 < p^2+p+1 < (p+1)^2$ and $(p-1)^2 < p^2-p+1 < p^2$ for $p \ge 2$ , so each lies strictly between two consecutive squares. This supplies the non-square input on the two cyclotomic factors of $\sigma(p^5)$ used in the $k=5$ square-free-index analysis.

Preamble

import Mathlib

Formal statement

namespace OddPerfectNumber.Kernel

theorem five_cyclotomic_factors_ne_square (p : Nat) (hp : 2 < p) :
    (¬ ∃ a, a ^ 2 = p ^ 2 + p + 1) ∧ (¬ ∃ b, b ^ 2 = p ^ 2 - p + 1) := by
  sorry

end OddPerfectNumber.Kernel

Source

Consecutive-square argument (Mathlib `Nat.not_exists_sq'`) for the two non-trivial cyclotomic factors of

\sigma(p^5)

in the

k=5

square-free-index reduction.

View graph