An odd nontrivial order forces the odd count to be a multiple of an odd number at most (p-1)/2
ProvedOddPerfectNumber.odd_order_odd_source_count_le_pfactorizationnumber-theoryperfect-numbers
Let p be a prime congruent to 1 modulo 4 and t a natural number with p not dividing t whose multiplicative order modulo p is greater than 1 and divides the odd natural number n. Then n is at least the order of t modulo p, so the odd count n is at least that order, and every such order is an odd divisor of (p-1)/2.
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber
theorem odd_order_odd_source_count_le_p {p t n : Nat} (hp : p.Prime) (hp4 : p % 4 = 1)
(hpt : Not (Dvd.dvd p t)) (hnodd : ¬ Even n) (hord : 1 < orderOf (t : ZMod p))
(hdiv : Dvd.dvd (orderOf (t : ZMod p)) n) :
orderOf (t : ZMod p) ≤ n ∧ Dvd.dvd (orderOf (t : ZMod p)) ((p - 1) / 2) := by
sorry
end OddPerfectNumber