No incoming -source when is a power of two
DisprovedOddPerfectNumber.Kernel.no_p_source_when_quarter_power_of_twoLet be prime with , and suppose is a power of two. Then no prime can satisfy .
Proof. gives , so and ; in particular is odd. By Fermat , and since and is odd, forces . If then is a power of two and also odd, so , i.e. . But then , and the proved theorem sigma_square_at_one_mod_p_not_dvd_p forbids from dividing when . Hence , which is the only possibility.
Consequence. The second Dris equation requires an incoming source of , since . For primes with a power of two this is impossible, so those are eliminated. Numerically, for the eliminated primes are exactly , and — in particular is ruled out, and survives neither. Primes with an odd factor in (e.g. ) are unaffected.
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber.Kernel
/-- If `p = 1 (mod 4)` and `(p-1)/4` is a power of two, then a prime `t` dividing the
three-term sum must satisfy `t = 1 (mod p)`. -/
theorem no_p_source_when_quarter_power_of_two (p t e k : Nat) (hp : p.Prime) (hp4 : p % 4 = 1)
(hq : t.Prime) (hquart : (p - 1) / 4 = 2 ^ k)
(hdiv : (p : Nat) ∣ 1 + t + t ^ (2 * e)) :
(t : ZMod p) = 1 := by
sorry
end OddPerfectNumber.Kernel