The 3-adic multiplicity of n^2-n+1 is exactly 1 when n is 2 mod 3
ProvedOddPerfectNumber.Kernel.vp_three_of_mod_two3-adiccyclotomick-fiveodd-perfectvaluation
If n is congruent to 2 modulo 3, then the exponent of 3 in n^2-n+1 is exactly one. Writing n = 3k+2 gives n^2-n+1 = 3(3k^2+3k+1), and the bracket is congruent to 1 modulo 3, so no further factor of 3 occurs.
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber.Kernel
theorem vp_three_of_mod_two (n : Nat) (hn : n % 3 = 2) :
(n ^ 2 - n + 1).factorization 3 = 1 := by sorry
end OddPerfectNumber.KernelSource
The companion 3-adic entry to vp_three_of_mod_one, needed by the two-prime squarefree-index residual. Verified by exact integer computation for every n <= 30000 in the residue class n % 3 = 2, with no counterexample.