2 and 5 are untouchable

A number m is untouchable if no n has aliquot sum s(n) = σ(n) - n = m. Both 2 and 5 are untouchable: a prime has s(p) = 1, and a composite n has the proper divisors 1 and n / minFac n ≥ √n, so s(n) ≥ 1 + √n; only finitely many n remain, and they are checked.

As a consequence, σ(x) mod x = 5 forces σ(x) ≥ 2x + 5: the case σ(x) = x + 5 of the open statement a 5 = 0 of OEIS A076495 (no x with σ(x) mod x = 5) is impossible, and what remains open is σ(x) = k x + 5 with k ≥ 2.

Main results

• Untouchable.untouchable_two: no n has sum of proper divisors 2
• Untouchable.untouchable_five: no n has sum of proper divisors 5
• Untouchable.two_mul_add_five_le_sigma: sigma x mod x = 5 forces sigma x >= 2x + 5

References

• OEIS A005114 (untouchable numbers); OEIS A076495 (smallest x with sigma(x) mod x = n; a(5) = 0 is open, searched beyond 1.5 * 10^14).

def Untouchable.IsUntouchable (m : ℕ) : Prop

m is untouchable when no natural number has aliquot sum m.

Equations

• Untouchable.IsUntouchable m = ∀ (n : ℕ), ∑ d ∈ n.properDivisors, d ≠ m

theorem Untouchable.untouchable_two : IsUntouchable 2

theorem Untouchable.untouchable_five : IsUntouchable 5

theorem Untouchable.two_mul_add_five_le_sigma {x : ℕ} (h : (ArithmeticFunction.sigma 1) x % x = 5) : 2 * x + 5 ≤ (ArithmeticFunction.sigma 1) x

If σ(x) mod x = 5, then σ(x) ≥ 2x + 5: the quotient ⌊σ(x)/x⌋ is at least 2, since the quotient 1 would make x have aliquot sum 5.