A 2-adic constraint on σ(n) = 2·σ*(n) (OEIS A063880)

If σ(n) = 2 · usigma(n) (usigma the sum of unitary divisors), some odd prime p divides n with exponent ≡ 3 (mod 4); in particular p³ ∣ n (for n = 108 = 2²·3³ it is p = 3). For every prime power p^k ∥ n, v₂(σ(p^k)) ≤ v₂(1 + p^k) unless p is odd and k ≡ 3 (mod 4); both σ and usigma are multiplicative, so without such a prime v₂(σ n) ≤ v₂(usigma n), against σ n = 2 · usigma n. This is a partial result towards the OPEN statements of formal-conjectures (n ≡ 108 (mod 216) and 108 the only primitive term), which are not proved here.

Main results

• OeisA63880.usigma_mul: the sum of unitary divisors is multiplicative
• OeisA63880.usigma_prime_pow: usigma(p^k) = 1 + p^k
• OeisA63880.exists_odd_prime_factorization_mod_four: sigma n = 2 usigma n forces an odd prime with exponent 3 mod 4
• OeisA63880.exists_odd_prime_cube_dvd: sigma n = 2 usigma n forces p^3 | n for some odd prime p

References

• OEIS A063880 (numbers n with sigma(n) = 2 usigma(n)); R. Stephan's observation that all terms are 108 mod 216 (2003), checked to 10^7 (R. G. Wilson v) and the uniqueness of the primitive 108 below 10^18 (A. Eldar, 2024) are conjectures/computations, not proofs.
• Definitions copied verbatim from google-deepmind/formal-conjectures, FormalConjectures/OEIS/63880.lean (open there).

def OeisA63880.unitaryDivisors (n : ℕ) : Finset ℕ

The set of unitary divisors of $n$: divisors $d$ such that $\gcd(d, n/d) = 1$.

Equations

• OeisA63880.unitaryDivisors n = {d ∈ n.divisors | d.Coprime (n / d)}

def OeisA63880.usigma (n : ℕ) : ℕ

The sum of unitary divisors of $n$, denoted $\text{usigma}(n)$.

Equations

• OeisA63880.usigma n = ∑ d ∈ OeisA63880.unitaryDivisors n, d

def OeisA63880.A (n : ℕ) : Prop

A number $n$ is in the sequence A063880 if $\sigma(n) = 2 \cdot \text{usigma}(n)$.

Equations

• OeisA63880.A n = (0 < n ∧ (ArithmeticFunction.sigma 1) n = 2 * OeisA63880.usigma n)

theorem OeisA63880.mem_unitaryDivisors {n d : ℕ} : d ∈ unitaryDivisors n ↔ (d ∣ n ∧ n ≠ 0) ∧ d.Coprime (n / d)

theorem OeisA63880.one_mem_unitaryDivisors {n : ℕ} (hn : 0 < n) : 1 ∈ unitaryDivisors n

theorem OeisA63880.usigma_pos {n : ℕ} (hn : 0 < n) : 0 < usigma n

theorem OeisA63880.usigma_mul {a b : ℕ} (ha : 0 < a) (hb : 0 < b) (hab : a.Coprime b) : usigma (a * b) = usigma a * usigma b

usigma is multiplicative.

theorem OeisA63880.usigma_prime_pow {p k : ℕ} (hp : Nat.Prime p) (hk : 0 < k) : usigma (p ^ k) = 1 + p ^ k

usigma (p ^ k) = 1 + p ^ k for k ≥ 1.

theorem OeisA63880.sum_range_mod_two (f : ℕ → ℕ) (hf : ∀ (i : ℕ), f i % 2 = 1) (n : ℕ) : (∑ i ∈ Finset.range n, f i) % 2 = n % 2

A sum of n odd numbers has the parity of n.

theorem OeisA63880.geom_even_split (p m : ℕ) : ∑ i ∈ Finset.range (2 * m), p ^ i = (1 + p) * ∑ j ∈ Finset.range m, p ^ (2 * j)

theorem OeisA63880.padicValNat_two_local {p k : ℕ} (hp : Nat.Prime p) (h : ¬(p ≠ 2 ∧ k % 4 = 3)) : padicValNat 2 (∑ i ∈ Finset.range (k + 1), p ^ i) ≤ padicValNat 2 (1 + p ^ k)

Local 2-adic inequality: v₂(σ(p^k)) ≤ v₂(1 + p^k) unless p is odd and k ≡ 3 (mod 4).

theorem OeisA63880.padicValNat_two_le (n : ℕ) : 0 < n → (∀ (p : ℕ), Nat.Prime p → p ≠ 2 → n.factorization p % 4 ≠ 3) → padicValNat 2 ((ArithmeticFunction.sigma 1) n) ≤ padicValNat 2 (usigma n)

The global inequality, by multiplicativity.

theorem OeisA63880.exists_odd_prime_factorization_mod_four {n : ℕ} (hA : A n) : ∃ (p : ℕ), Nat.Prime p ∧ p ≠ 2 ∧ n.factorization p % 4 = 3

Main result. Every term of A063880 has an odd prime factor whose exponent is ≡ 3 (mod 4).

theorem OeisA63880.exists_odd_prime_cube_dvd {n : ℕ} (hA : A n) : ∃ (p : ℕ), Nat.Prime p ∧ p ≠ 2 ∧ p ^ 3 ∣ n

Corollary: every term of A063880 is divisible by the cube of an odd prime.