Primitive non-deficient numbers

TheoremPrime-power bound for primitive non-deficient numbers#✓fully proved

Let \(\sigma(m)\) denote the sum of the divisors of \(m\). Let \(n\) be a positive integer that is non-deficient, \(\sigma(n) \ge 2n\), and primitive, meaning that every divisor \(m\) of \(n\) with \(m < n\) is deficient, \(\sigma(m) < 2m\). Let \(k\) be the number of distinct prime factors of \(n\) and \(R\) their product. Then \(n\) has a prime factor \(p\) with \(p^{v_p(n) + 1} < 2kR\), where \(v_p(n)\) is the exponent of \(p\) in \(n\).

theorem primitive_nondeficient_prime_power_bound
    (n : ℕ) (hn : n ≠ 0)
    (hnondef : 2 * n ≤ ∑ d ∈ Nat.divisors n, d)
    (hprim : ∀ m ∈ Nat.divisors n, m < n → ∑ d ∈ Nat.divisors m, d < 2 * m) :
    ∃ p ∈ n.primeFactors,
      p ^ (n.factorization p + 1) < 2 * n.primeFactors.card * ∏ q ∈ n.primeFactors, q
Sources
  • Joshua Zelinsky, "Must a Primitive Non-Deficient Number Always Have a Small Component?," Journal of Integer Sequences 29 (2026), Article 26.4.3, Theorem, equation, lines 107–109, https://cs.uwaterloo.ca/journals/JIS/VOL29/Zelinsky/zel14.tex

DefinitionNon-deficient number#✓fully proved

A natural number \(n\) is non-deficient when \(n \ne 0\) and \(\sigma(n) \ge 2n\), where \(\sigma(n)\) is the sum of the positive divisors of \(n\).

Positivity is part of the notion: \(0\) has no divisors in this convention, so the inequality alone would make \(0\) non-deficient.

def IsNondeficient (n : ℕ) : Prop :=
  n ≠ 0 ∧ 2 * n ≤ ∑ d ∈ Nat.divisors n, d
Used by 2
Used byGrün's bound for non-deficient numbers · Primitive non-deficient number

DefinitionPrimitive non-deficient number#✓fully proved

A natural number \(n\) is primitive non-deficient when it is non-deficient and every proper divisor \(m\) of \(n\) (a divisor with \(m < n\)) is deficient, that is, \(\sigma(m) < 2m\), where \(\sigma(m)\) is the sum of the positive divisors of \(m\).

def IsPrimitiveNondeficient (n : ℕ) : Prop :=
  IsNondeficient n ∧
    ∀ m ∈ Nat.divisors n, m < n → ∑ d ∈ Nat.divisors m, d < 2 * m
Uses 1 · Used by 9
Statement usesNon-deficient number
Used byBound on \(H(n)\) for primitive non-deficient numbers by the least prime factor · Lower bound on the prime reciprocal sum of an odd primitive non-deficient number · Lower bound on the prime reciprocal sum of a primitive non-deficient number · Upper bound on the prime reciprocal sum of a primitive non-deficient number with one odd exponent · Generalized Puchta lemma · Small component for odd primitive non-deficient numbers with three or four prime factors · Even primitive non-deficient numbers with two prime factors · Dichotomy for odd primitive non-deficient numbers · The power of 2 in an even primitive non-deficient number is below its radical

DefinitionAbundancy index#✓fully proved

For a natural number \(n\), the abundancy index is the rational number \(h(n) = \sigma(n)/n\), where \(\sigma(n)\) is the sum of the positive divisors of \(n\).

At \(n = 0\) this gives \(h(0) = 0\), since division by zero is \(0\) in \(\mathbb{Q}\); the abundancy index is only meaningful for positive \(n\).

noncomputable def abundancyIndex (n : ℕ) : ℚ :=
  ((∑ d ∈ Nat.divisors n, d : ℕ) : ℚ) / (n : ℚ)
Used by 2
Used bySuryanarayana's bound for \(H(n)/h(n)\) with one odd exponent · Abundancy ratio at an exactly dividing prime power

DefinitionProduct of \(p/(p-1)\) over the prime factors#✓fully proved

For a natural number \(n\), let \(H(n) = \prod_p p/(p-1)\) in \(\mathbb{Q}\), the product over the distinct primes \(p\) dividing \(n\). For \(n = 0\) the product is empty (\(0\) is taken to have no prime factors), so \(H(0) = 1\).

noncomputable def abundancySup (n : ℕ) : ℚ :=
  ∏ p ∈ n.primeFactors, (p : ℚ) / ((p : ℚ) - 1)
Used by 9
Used bySuryanarayana's bound for \(H(n)/h(n)\) with one odd exponent · Bound on \(H(n)\) for primitive non-deficient numbers by the least prime factor · No odd prime \(q\) lifts \(H\) of the odd part of \(q + 1\) across \(2\) · Bound on the prime product of an odd perfect number via its least prime factor · Suryanarayana's bounds on the prime product of an odd perfect number · Surplus of an odd perfect number with least prime factor at least 11 · Lower bound on the prime reciprocal sum of an odd primitive non-deficient number · Lower bound on the prime reciprocal sum of a primitive non-deficient number · Generalized Puchta lemma

TheoremEven primitive non-deficient numbers with two prime factors#●ready to prove

Let \(p\) be an odd prime and \(a\) a natural number. Then \(2^a p\) is primitive non-deficient if and only if \(2^a < p \le 2^{a+1} - 1\).

theorem_wanted isPrimitiveNondeficient_two_pow_mul_prime_iff
    (a p : ℕ) (hp : p.Prime) (hpo : p ≠ 2) :
    IsPrimitiveNondeficient (2 ^ a * p) ↔
      2 ^ a < p ∧ p ≤ 2 ^ (a + 1) - 1
Sources
  • Joshua Zelinsky, "Must a Primitive Non-Deficient Number Always Have a Small Component?", Lemma, first part.
Uses 1
Statement usesPrimitive non-deficient number

TheoremOdd numbers with two prime factors are deficient#●ready to prove

If \(n\) is an odd natural number with exactly two distinct prime divisors, then \(\sigma(n) < 2n\), where \(\sigma(n)\) is the sum of the positive divisors of \(n\).

theorem_wanted deficient_of_odd_card_primeFactors_eq_two
    (n : ℕ) (hno : Odd n) (hk : n.primeFactors.card = 2) :
    ∑ d ∈ Nat.divisors n, d < 2 * n
Sources
  • Joshua Zelinsky, "Must a Primitive Non-Deficient Number Always Have a Small Component?", Lemma, second part.

TheoremSmall component for odd primitive non-deficient numbers with three or four prime factors#●ready to prove

Let \(n\) be an odd primitive non-deficient number with exactly \(3\) or exactly \(4\) distinct prime factors, and let \(R\) be the product of the distinct prime factors of \(n\). Then some prime factor \(p\) of \(n\) satisfies \(p^{a+1} < 2R\), where \(a\) is the exponent of \(p\) in \(n\).

theorem_wanted exists_pow_factorization_add_one_lt_two_mul_radical
    (n : ℕ) (hno : Odd n) (hn : IsPrimitiveNondeficient n)
    (hk : n.primeFactors.card = 3 ∨ n.primeFactors.card = 4) :
    ∃ p ∈ n.primeFactors,
      p ^ (n.factorization p + 1) < 2 * ∏ q ∈ n.primeFactors, q
Sources
  • Joshua Zelinsky, "Must a Primitive Non-Deficient Number Always Have a Small Component?", Lemma.
Uses 1
Statement usesPrimitive non-deficient number

TheoremGrün's bound for non-deficient numbers#●ready to prove

Let \(n\) be a non-deficient number with \(k\) distinct prime factors, the least of which is \(p_1\). Then \(\tfrac{3}{2} p_1 - 2 < k\), and if \(p_1 \ge 5\) then \(p_1 + 2 \le k\).

theorem_wanted grun_bounds_of_isNondeficient
    (n p₁ : ℕ) (hn : IsNondeficient n)
    (hp₁ : p₁ ∈ n.primeFactors)
    (hmin : ∀ q ∈ n.primeFactors, p₁ ≤ q) :
    (3 : ℚ) / 2 * (p₁ : ℚ) - 2 < (n.primeFactors.card : ℚ) ∧
      (5 ≤ p₁ → p₁ + 2 ≤ n.primeFactors.card)
Sources
  • Joshua Zelinsky, "Must a Primitive Non-Deficient Number Always Have a Small Component?", Lemma.
Uses 1
Statement usesNon-deficient number

TheoremThe power of 2 in an even primitive non-deficient number is below its radical#●ready to prove

Let \(n\) be an even primitive non-deficient number, that is, a positive integer with \(\sigma(n) \ge 2n\) all of whose proper divisors \(m\) satisfy \(\sigma(m) < 2m\), where \(\sigma\) is the sum of divisors. If \(2^a\) is the largest power of \(2\) dividing \(n\) and \(R\) is the product of the distinct primes dividing \(n\), then \(2^{a+1} < R\).

theorem_wanted two_pow_factorization_add_one_lt_radical
    (n : ℕ) (hne : Even n)
    (hn : IsPrimitiveNondeficient n) :
    2 ^ (n.factorization 2 + 1) < ∏ q ∈ n.primeFactors, q
Sources
  • Joshua Zelinsky, "Must a Primitive Non-Deficient Number Always Have a Small Component?", Proposition.
Uses 1
Statement usesPrimitive non-deficient number

TheoremZelinsky's reciprocal bound#●ready to prove

For real numbers \(k\) and \(m\) with \(k \ge 2\) and \(0 < m < 1/(k(k+1))\), we have \(1/(1 - km) < 1 + (k+1)m\).

theorem_wanted one_div_one_sub_mul_lt_add
    (k m : ℝ) (hk : 2 ≤ k) (hm0 : 0 < m)
    (hm : m < 1 / (k * (k + 1))) :
    1 / (1 - k * m) < 1 + (k + 1) * m
Sources
  • Joshua Zelinsky, "Must a Primitive Non-Deficient Number Always Have a Small Component?", Lemma.

TheoremAbundancy ratio at an exactly dividing prime power#●ready to prove

Let \(n\) be a positive integer, \(p\) a prime and \(a \ge 1\) an integer such that \(p^a\) exactly divides \(n\) (that is, \(p^a \mid n\) and \(p^{a+1} \nmid n\)). Then \(h(n)/h(n/p) \le 1 + 1/p^a\), where \(h(m) = \sigma(m)/m\) is the abundancy index and \(\sigma(m)\) is the sum of the positive divisors of \(m\).

theorem_wanted abundancyIndex_div_le
    (n p a : ℕ) (hn0 : 0 < n) (hp : p.Prime) (ha : 1 ≤ a)
    (hpa : n.factorization p = a) :
    abundancyIndex n / abundancyIndex (n / p) ≤
      1 + 1 / (p : ℚ) ^ a
Sources
  • Joshua Zelinsky, "Must a Primitive Non-Deficient Number Always Have a Small Component?", Lemma.
Uses 1
Statement usesAbundancy index

TheoremGeneralized Puchta lemma#●ready to prove

Let \(n\) be a primitive non-deficient number with \(k\) distinct prime factors, the least of which is \(p_1\), and suppose that \((p_1, k) \ne (3, 3)\). Let \(\alpha\) be a rational number with \(0 < \alpha < 1\) such that \(H(n) \ge 2 + \alpha\), where \(H(n) = \prod_p p/(p-1)\) is the product over the distinct primes \(p\) dividing \(n\). Then some prime factor \(p\) of \(n\) satisfies \(p^{a+1} < \max\bigl(2(k + 2 + p_1)/\alpha,\ k(k+1)\bigr)\), where \(a\) is the exponent of \(p\) in \(n\).

theorem_wanted exists_pow_factorization_add_one_lt_max
    (n p₁ : ℕ) (hn : IsPrimitiveNondeficient n)
    (hp₁ : p₁ ∈ n.primeFactors)
    (hmin : ∀ q ∈ n.primeFactors, p₁ ≤ q)
    (hne : ¬ (p₁ = 3 ∧ n.primeFactors.card = 3))
    (α : ℚ) (hα0 : 0 < α) (hα1 : α < 1)
    (hH : 2 + α ≤ abundancySup n) :
    ∃ p ∈ n.primeFactors,
      ((p ^ (n.factorization p + 1) : ℕ) : ℚ) <
        max
          (2 * ((n.primeFactors.card : ℚ) + 2 + (p₁ : ℚ)) / α)
          ((n.primeFactors.card : ℚ) *
            ((n.primeFactors.card : ℚ) + 1))
Sources
  • Joshua Zelinsky, "Must a Primitive Non-Deficient Number Always Have a Small Component?", Lemma.
Uses 2
Statement usesPrimitive non-deficient number · Product of \(p/(p-1)\) over the prime factors

TheoremDichotomy for odd primitive non-deficient numbers#●ready to prove

Let \(n\) be an odd primitive non-deficient number, that is, a positive integer with \(\sigma(n) \ge 2n\) all of whose proper divisors \(m\) satisfy \(\sigma(m) < 2m\), where \(\sigma\) is the sum of divisors. Let \(k\) be the number of distinct prime factors of \(n\), let \(p_1\) and \(p_k\) be its least and greatest prime factors, and let \(R\) be the product of the distinct primes dividing \(n\). Then either \(p_k < \sqrt{R}\), or some prime \(p\) dividing \(n\) satisfies \(p^{a+1} < (k + 2 + p_1)(p_k - 1)\), where \(a\) is the exponent of \(p\) in \(n\).

theorem_wanted max_primeFactor_lt_sqrt_radical_or_exists_pow_lt
    (n p₁ pK : ℕ) (hno : Odd n)
    (hn : IsPrimitiveNondeficient n)
    (hp₁ : p₁ ∈ n.primeFactors)
    (hmin : ∀ q ∈ n.primeFactors, p₁ ≤ q)
    (hpK : pK ∈ n.primeFactors)
    (hmax : ∀ q ∈ n.primeFactors, q ≤ pK) :
    (pK : ℝ) < Real.sqrt ((∏ q ∈ n.primeFactors, q : ℕ) : ℝ) ∨
      ∃ p ∈ n.primeFactors,
        p ^ (n.factorization p + 1) <
          (n.primeFactors.card + 2 + p₁) * (pK - 1)
Sources
  • Joshua Zelinsky, "Must a Primitive Non-Deficient Number Always Have a Small Component?", Proposition.
Uses 1
Statement usesPrimitive non-deficient number
5 fully proved9 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.