Conjectures associated with A063880

A063880 lists numbers $n$ such that $\sigma(n) = 2 \cdot \text{usigma}(n)$, where $\sigma(n)$ is the sum of all divisors and $\text{usigma}(n)$ is the sum of unitary divisors.

Equivalently, these are numbers whose unitary and non-unitary divisors have equal sum.

The conjectures state that all members satisfy $n \equiv 108 \pmod{216}$, and that all primitive terms (those whose proper divisors aren't in the sequence) are powerful numbers, with $108$ being the only primitive term.

References: A063880

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)

def OeisA63880.A : Set ℕ

The set of numbers in the sequence A063880.

Equations

• OeisA63880.A = {n : ℕ | OeisA63880.a n}

@[reducible, inline]

abbrev OeisA63880.isPrimitiveTerm (n : ℕ) : Prop

A term $n$ is primitive if no proper divisor of $n$ is in the sequence.

Equations

• OeisA63880.isPrimitiveTerm n = OeisA63880.A.IsPrimitive n

theorem OeisA63880.a_108 : a 108

$108$ is in the sequence A063880.

theorem OeisA63880.a_540 : a 540

$540$ is in the sequence A063880.

theorem OeisA63880.a_756 : a 756

$756$ is in the sequence A063880.

theorem OeisA63880.isPrimitiveTerm_108 : isPrimitiveTerm 108

$108$ is a primitive term.

theorem OeisA63880.mod_216_of_a {n : ℕ} (h : a n) : n % 216 = 108

All members of the sequence satisfy $n \equiv 108 \pmod{216}$.

theorem OeisA63880.powerful_of_isPrimitiveTerm {n : ℕ} (h : isPrimitiveTerm n) : n.Powerful

All primitive terms are powerful numbers.

theorem OeisA63880.unique_primitive_108 {n : ℕ} (h : isPrimitiveTerm n) : n = 108

$108$ is the only primitive term.

theorem OeisA63880.a_of_primitive_mul_squarefree (m s : ℕ) (hm : isPrimitiveTerm m) (hs : Squarefree s) (hcoprime : m.Coprime s) : a (m * s)

If $m$ is a primitive term and $s$ is squarefree with $\gcd(m, s) = 1$, then $m \cdot s$ is in the sequence.

theorem OeisA63880.exists_primitive_of_a {n : ℕ} (h : a n) : ∃ (m : ℕ) (s : ℕ), isPrimitiveTerm m ∧ Squarefree s ∧ m.Coprime s ∧ n = m * s

Non-primitive terms have the form $m \cdot s$ where $m$ is primitive and $s$ is squarefree with $\gcd(m, s) = 1$.