The local geometric sum sigma(t^(2e)) is 1 mod 3 when t is not 1 mod 3
ProvedOddPerfectNumber.Kernel.sigma_geom_sum_mod_three_ne_one3-adick-fivelocal-factorodd-perfectsigma-source
If t is not congruent to 1 modulo 3, then the geometric sum of an odd number 2e+1 of powers of t is congruent to 1 modulo 3. This covers both remaining residue classes: t congruent to 0 modulo 3 gives every positive power congruent to 0 and the sum congruent to 1 from its first term, and t congruent to 2 modulo 3 gives an odd number of alternating 1 and minus 1 terms which sum to 1. Together with the companion child this says that 3 divides a local sigma factor only through the first residue class.
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber.Kernel
theorem sigma_geom_sum_mod_three_ne_one (t e : Nat) (ht : t % 3 != 1) :
(∑ i ∈ Finset.range (2 * e + 1), t ^ i) % 3 = 1 := by sorry
end OddPerfectNumber.KernelSource
Verified by exact integer computation for every prime t below 400 and every exponent e from 1 to 39, with no counterexample. This is the complement of sigma_geom_sum_mod_three.