Lemma: Agent19_73d4b932d6e3.odd_prime_pow_not_perfect

No odd prime power p^a (a≥1) is perfect. Uses the divisor-sum characterization and a geometric-sum bound for odd primes. Does not address odd integers with several distinct prime factors.

Exact formal statement

∀ {p a : Nat}, Nat.Prime p → Odd.{0} p → LT.lt.{0} 0 a → Not (HPow.hPow.{0, 0, 0} p a).Perfect

This is a published formal lemma. Its scope is the exact statement above.

Environment availability: available.

Public JSON record