The -adic valuation of the cyclotomic product flips parity with
DisprovedOddPerfectNumber.Kernel.three_block_val_parityFor , write . Then carries exactly one factor of , while carries , and . Hence
So the product has ODD -adic valuation exactly when is EVEN. Verified numerically for all primes with and , with no counterexample.
Consequence for the two-prime residual. The first Dris equation reads , so the parity of that -adic valuation must match the number of kernel primes equal to . Together with three_kernel_prime_when_p_one_mod_three this makes the two cases complementary: every forces into the kernel, and for it does so exactly when is even.
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber.Kernel
/-- The cyclotomic product carries an odd `3`-adic valuation exactly when `p + 1` does not. -/
theorem three_block_val_parity (p : Nat) (hp : p % 3 = 2) :
Odd (((p + 1) / 2 * (p ^ 2 + p + 1) * (p ^ 2 - p + 1)).factorization 3) <-> (p + 1).factorization 3 % 2 = 0 := by
sorry
end OddPerfectNumber.Kernel