Distribution of cyclic numbers

DefinitionCyclic numbers#✓fully proved

A positive integer \(n\) is cyclic when \(\gcd(n, \varphi(n)) = 1\), where \(\varphi\) is Euler's totient function.

def IsCyclicNumber (n : ℕ) : Prop :=
  0 < n ∧ n.Coprime n.totient
Used by 11
Used byAsymptotic count of cyclic and composite cyclic numbers · The cyclic counting functions vary regularly with index one · Gaps between cyclic numbers under the Riemann hypothesis · Mean and variance of the cyclic numbers · Generalized Taylor's law for cyclic numbers · Relation between the moments of the cyclic numbers · Taylor's law for cyclic numbers · Cohen's Oppermann conjecture for cyclic numbers · Cyclic numbers in the left Oppermann interval · Cyclic numbers in the right Oppermann interval · Power sums of cyclic numbers

DefinitionCyclic numbers in the left Oppermann interval#✓fully proved

For a natural number \(n\), this is the number of cyclic numbers \(k\) with \(n^2 - n \le k \le n^2\).

def oppermannCyclicCountLeft (n : ℕ) : ℕ :=
  letI : DecidablePred IsCyclicNumber := fun k => by
    unfold IsCyclicNumber
    infer_instance
  ((Finset.Icc (n ^ 2 - n) (n ^ 2)).filter IsCyclicNumber).card
Uses 1 · Used by 1
Statement usesCyclic numbers
Used byCohen's Oppermann conjecture for cyclic numbers

DefinitionCyclic numbers in the right Oppermann interval#✓fully proved

For a natural number \(n\), this is the number of cyclic numbers \(k\) with \(n^2 \le k \le n^2 + n\).

def oppermannCyclicCountRight (n : ℕ) : ℕ :=
  letI : DecidablePred IsCyclicNumber := fun k => by
    unfold IsCyclicNumber
    infer_instance
  ((Finset.Icc (n ^ 2) (n ^ 2 + n)).filter IsCyclicNumber).card
Uses 1 · Used by 1
Statement usesCyclic numbers
Used byCohen's Oppermann conjecture for cyclic numbers

DefinitionLeft-hand approximation for cyclic numbers near squares#✓fully proved

Let \(\gamma\) be the Euler–Mascheroni constant and, for real \(x\), let \(L(x) = \log \log \log (x^2)\). The left-hand approximation is the function of the real variable \(x\) given by

\[ \frac{x}{e^{\gamma} L(x)} \left(1 - \frac{\gamma}{L(x)}\right). \]

Here \(\log y\) means \(\log |y|\), with \(\log 0 = 0\), and a quotient by \(0\) is \(0\), so the expression is defined for every real \(x\). J. E. Cohen conjectures that, at \(x = n\), it is asymptotic to the number of cyclic numbers in \([n^2 - n, n^2]\).

noncomputable def oppermannCyclicLeftApproximation (x : ℝ) : ℝ :=
  x / (Real.exp Real.eulerMascheroniConstant *
    Real.log (Real.log (Real.log (x ^ 2)))) *
    (1 - Real.eulerMascheroniConstant /
      Real.log (Real.log (Real.log (x ^ 2))))
Used by 1
Used byCohen's Oppermann conjecture for cyclic numbers

DefinitionSimplified approximation for cyclic numbers near squares#✓fully proved

Let \(\gamma\) be the Euler–Mascheroni constant and, for real \(x\), let \(L(x) = \log \log \log x\). The simplified approximation is the function of the real variable \(x\) given by

\[ \frac{x}{e^{\gamma} L(x)} \left(1 - \frac{\gamma}{L(x)}\right). \]

Here \(\log y\) means \(\log |y|\), with \(\log 0 = 0\), and a quotient by \(0\) is \(0\), so the expression is defined for every real \(x\). J. E. Cohen conjectures that, at \(x = n\), it is asymptotic to the number of cyclic numbers in \([n^2 - n, n^2]\) and to the number in \([n^2, n^2 + n]\).

noncomputable def oppermannCyclicApproximation (x : ℝ) : ℝ :=
  x / (Real.exp Real.eulerMascheroniConstant *
    Real.log (Real.log (Real.log x))) *
    (1 - Real.eulerMascheroniConstant /
      Real.log (Real.log (Real.log x)))
Used by 1
Used byCohen's Oppermann conjecture for cyclic numbers

DefinitionRight-hand approximation for cyclic numbers near squares#✓fully proved

Let \(\gamma\) be the Euler–Mascheroni constant and, for real \(x\), let \(L(x) = \log \log \log (x(x+1))\). The right-hand approximation is the function of the real variable \(x\) given by

\[ \frac{x}{e^{\gamma} L(x)} \left(1 - \frac{\gamma}{L(x)}\right). \]

Here \(\log y\) means \(\log |y|\), with \(\log 0 = 0\), and a quotient by \(0\) is \(0\), so the expression is defined for every real \(x\). J. E. Cohen conjectures that, at \(x = n\), it is asymptotic to the number of cyclic numbers in \([n^2, n^2 + n]\).

noncomputable def oppermannCyclicRightApproximation (x : ℝ) : ℝ :=
  x / (Real.exp Real.eulerMascheroniConstant *
    Real.log (Real.log (Real.log (x * (x + 1))))) *
    (1 - Real.eulerMascheroniConstant /
      Real.log (Real.log (Real.log (x * (x + 1)))))
Used by 1
Used byCohen's Oppermann conjecture for cyclic numbers

TheoremAsymptotic count of cyclic and composite cyclic numbers#●ready to prove

For real \(x\), let \(A(x)\) be the number of cyclic numbers \(m\) with \(1 \le m \le x\), and let \(cc(x)\) be the number of composite cyclic numbers \(m \le x\), that is, cyclic numbers \(m > 1\) that are not prime. Then, as \(x \to \infty\), \(A(x) \sim cc(x)\) and \(cc(x) \sim x e^{-\gamma} / \log \log \log x\), where \(\gamma\) is the Euler–Mascheroni constant.

public theorem_wanted cyclicCount_isEquivalent_compositeCyclicCount :
    let A : ℝ → ℝ := fun x => (((Finset.Icc 1 ⌊x⌋₊).filter IsCyclicNumber).card : ℝ)
    let cc : ℝ → ℝ := fun x =>
      (((Finset.Icc 1 ⌊x⌋₊).filter fun m => IsCyclicNumber m ∧ 1 < m ∧ ¬m.Prime).card : ℝ)
    IsEquivalent atTop A cc ∧
      IsEquivalent atTop cc (fun x => x * Real.exp (-Real.eulerMascheroniConstant) /
        Real.log (Real.log (Real.log x)))
Sources
  • John M. Campbell and Joel E. Cohen, Cyclic Numbers and Gaps, INTEGERS 25 (2025), Article A23, Lemma 1.
Uses 1
Statement usesCyclic numbers

TheoremThe cyclic counting functions vary regularly with index one#●ready to prove

For real \(x\), let \(A(x)\) be the number of cyclic numbers \(m\) with \(1 \le m \le x\), let \(\pi(x)\) be the number of primes \(p \le x\), and let \(cc(x)\) be the number of composite cyclic numbers \(m \le x\), that is, cyclic numbers \(m > 1\) that are not prime. Then for every real \(\lambda > 0\), each of \(A(\lambda x) / A(x)\), \(\pi(\lambda x) / \pi(x)\) and \(cc(\lambda x) / cc(x)\) tends to \(\lambda\) as \(x \to \infty\).

Every prime is cyclic, so \(\pi(x)\) is also the number of prime cyclic numbers \(\le x\).

public theorem_wanted cyclicCountingFunctions_regularlyVarying_index_one :
    let A : ℝ → ℝ := fun x => (((Finset.Icc 1 ⌊x⌋₊).filter IsCyclicNumber).card : ℝ)
    let piFun : ℝ → ℝ := fun x => (Nat.primeCounting ⌊x⌋₊ : ℝ)
    let cc : ℝ → ℝ := fun x =>
      (((Finset.Icc 1 ⌊x⌋₊).filter fun m => IsCyclicNumber m ∧ 1 < m ∧ ¬m.Prime).card : ℝ)
    ∀ lam : ℝ, 0 < lam →
      Tendsto (fun x => A (lam * x) / A x) atTop (𝓝 lam) ∧
      Tendsto (fun x => piFun (lam * x) / piFun x) atTop (𝓝 lam) ∧
      Tendsto (fun x => cc (lam * x) / cc x) atTop (𝓝 lam)
Sources
  • John M. Campbell and Joel E. Cohen, Cyclic Numbers and Gaps, INTEGERS 25 (2025), Article A23, Theorem 1.
Uses 1
Statement usesCyclic numbers

TheoremTaylor's law for cyclic numbers#●ready to prove

Let \(c_1 < c_2 < \cdots\) be the cyclic numbers in increasing order, so \(c_1 = 1\). For \(n \ge 1\) let \(m(c,n) = \frac{1}{n} \sum_{i=1}^{n} c_i\) be the mean of \(c_1, \dots, c_n\), and for \(n \ge 2\) let \(v(c,n) = \frac{1}{n-1} \sum_{i=1}^{n} (c_i - m(c,n))^2\) be their variance. Then for every real \(b\), as \(n \to \infty\), \(v(c,n) / m(c,n)^b\) tends to \(\infty\) if \(b < 2\), to \(1/3\) if \(b = 2\), and to \(0\) if \(b > 2\).

public theorem_wanted cyclicNumbers_variance_div_mean_rpow_tendsto :
    let c : ℕ → ℝ := fun n => (Nat.nth IsCyclicNumber (n - 1) : ℝ)
    let mean : ℕ → ℝ := fun n => (∑ i ∈ Finset.Icc 1 n, c i) / n
    let var : ℕ → ℝ := fun n => (∑ i ∈ Finset.Icc 1 n, (c i - mean n) ^ 2) / (n - 1)
    ∀ b : ℝ,
      (b < 2 → Tendsto (fun n => var n / mean n ^ b) atTop atTop) ∧
      (b = 2 → Tendsto (fun n => var n / mean n ^ b) atTop (𝓝 (1 / 3))) ∧
      (2 < b → Tendsto (fun n => var n / mean n ^ b) atTop (𝓝 0))
Sources
  • John M. Campbell and Joel E. Cohen, Cyclic Numbers and Gaps, INTEGERS 25 (2025), Article A23, Theorem 1.
Uses 1
Statement usesCyclic numbers

TheoremMean and variance of the cyclic numbers#●ready to prove

Let \(c_1 < c_2 < \cdots\) be the cyclic numbers in increasing order, so \(c_1 = 1\). For \(n \ge 1\) let \(m(c,n) = \frac{1}{n} \sum_{i=1}^{n} c_i\) be the mean of \(c_1, \dots, c_n\), and for \(n \ge 2\) let \(v(c,n) = \frac{1}{n-1} \sum_{i=1}^{n} (c_i - m(c,n))^2\) be their variance. Then, as \(n \to \infty\), \(m(c,n) \sim c_n / 2\) and \(v(c,n) \sim c_n^2 / 12\).

public theorem_wanted cyclicNumbers_mean_variance_isEquivalent :
    let c : ℕ → ℝ := fun n => (Nat.nth IsCyclicNumber (n - 1) : ℝ)
    let mean : ℕ → ℝ := fun n => (∑ i ∈ Finset.Icc 1 n, c i) / n
    let var : ℕ → ℝ := fun n => (∑ i ∈ Finset.Icc 1 n, (c i - mean n) ^ 2) / (n - 1)
    IsEquivalent atTop mean (fun n => c n / 2) ∧
      IsEquivalent atTop var (fun n => c n ^ 2 / 12)
Sources
  • John M. Campbell and Joel E. Cohen, Cyclic Numbers and Gaps, INTEGERS 25 (2025), Article A23, Theorem 1.
Uses 1
Statement usesCyclic numbers

TheoremRelation between the moments of the cyclic numbers#●ready to prove

Let \(c_1 < c_2 < \cdots\) be the cyclic numbers in increasing order, so \(c_1 = 1\), and for \(n \ge 1\) and a natural number \(k\) let \(\mu'(c,n,k) = \frac{1}{n} \sum_{i=1}^{n} c_i^k\) be the \(k\)-th moment of \(c_1, \dots, c_n\). Then for all natural numbers \(j \ge 1\) and \(k\), as \(n \to \infty\),

\[ \mu'(c,n,k) \sim \frac{(j+1)^{k/j}}{k+1} \, \mu'(c,n,j)^{k/j}. \]
public theorem_wanted cyclicNumbers_moment_isEquivalent_moment_rpow (j k : ℕ) (hj : 1 ≤ j) :
    let c : ℕ → ℝ := fun n => (Nat.nth IsCyclicNumber (n - 1) : ℝ)
    let μ : ℕ → ℕ → ℝ := fun n k => (∑ i ∈ Finset.Icc 1 n, c i ^ k) / n
    IsEquivalent atTop (fun n => μ n k)
      (fun n => ((j : ℝ) + 1) ^ ((k : ℝ) / j) / (k + 1) * μ n j ^ ((k : ℝ) / j))
Sources
  • John M. Campbell and Joel E. Cohen, Cyclic Numbers and Gaps, INTEGERS 25 (2025), Article A23, Theorem 1.
Uses 1
Statement usesCyclic numbers

TheoremGeneralized Taylor's law for cyclic numbers#●ready to prove

Let \(c_1 < c_2 < \cdots\) be the cyclic numbers in increasing order, so \(c_1 = 1\). For \(n \ge 1\) and a natural number \(k\) let \(\mu'(c,n,k) = \frac{1}{n} \sum_{i=1}^{n} c_i^k\) be the \(k\)-th moment of \(c_1, \dots, c_n\), and let \(m(c,n) = \mu'(c,n,1)\) be their mean. Then for every natural number \(k\), as \(n \to \infty\),

\[ \mu'(c,n,k) \sim \frac{2^k}{1+k} \, m(c,n)^k. \]
public theorem_wanted cyclicNumbers_moment_isEquivalent_mean_pow (k : ℕ) :
    let c : ℕ → ℝ := fun n => (Nat.nth IsCyclicNumber (n - 1) : ℝ)
    let mean : ℕ → ℝ := fun n => (∑ i ∈ Finset.Icc 1 n, c i) / n
    IsEquivalent atTop (fun n : ℕ => (∑ i ∈ Finset.Icc 1 n, c i ^ k) / n)
      (fun n => (2 : ℝ) ^ k / (1 + k) * mean n ^ k)
Sources
  • John M. Campbell and Joel E. Cohen, Cyclic Numbers and Gaps, INTEGERS 25 (2025), Article A23, Theorem 1.
Uses 1
Statement usesCyclic numbers

TheoremGaps between cyclic numbers under the Riemann hypothesis#●ready to prove

Assume the Riemann hypothesis. Let \(c_1 < c_2 < \cdots\) be the cyclic numbers in increasing order and \(p_1 < p_2 < \cdots\) the primes in increasing order. Then the gaps \(d_n = c_{n+1} - c_n\) between consecutive cyclic numbers satisfy \(d_n = o(\sqrt{p_n} \log p_n)\) as \(n \to \infty\).

public theorem_wanted cyclicNumber_gap_isLittleO_of_riemannHypothesis
    (hRH : RiemannHypothesis) :
    let c : ℕ → ℝ := fun n => (Nat.nth IsCyclicNumber (n - 1) : ℝ)
    let p : ℕ → ℝ := fun n => (Nat.nth Nat.Prime (n - 1) : ℝ)
    (fun n => c (n + 1) - c n) =o[atTop] (fun n => Real.sqrt (p n) * Real.log (p n))
Sources
  • John M. Campbell and Joel E. Cohen, Cyclic Numbers and Gaps, INTEGERS 25 (2025), Article A23, Theorem 2.
Uses 1
Statement usesCyclic numbers

TheoremCohen's Oppermann conjecture for cyclic numbers#●ready to prove

For every natural number \(n > 1\) there are cyclic numbers \(c\) and \(c'\) with \(n^2 - n < c < n^2 < c' < n^2 + n\). Moreover, let \(C_L(n)\) and \(C_R(n)\) be the numbers of cyclic numbers in \([n^2 - n, n^2]\) and in \([n^2, n^2 + n]\), and let \(A_L\), \(A_R\) and \(A\) be the left-hand, right-hand and simplified approximations for cyclic numbers near squares. Then, as \(n \to \infty\) through the natural numbers, \(C_L(n) \sim A_L(n)\), \(A_L(n) \sim A(n)\), \(C_R(n) \sim A_R(n)\) and \(A_R(n) \sim A(n)\).

MetaMathlibExt.oppermannAnalogForCyclicNumbers · 16 lines 
theorem_wanted oppermannAnalogForCyclicNumbers :
    (∀ n : ℕ, 1 < n →
      ∃ c c' : ℕ, IsCyclicNumber c ∧ n ^ 2 - n < c ∧ c < n ^ 2 ∧
        IsCyclicNumber c' ∧ n ^ 2 < c' ∧ c' < n ^ 2 + n) ∧
    Asymptotics.IsEquivalent (Filter.atTop : Filter ℕ)
      (fun n => (oppermannCyclicCountLeft n : ℝ))
      (fun n => oppermannCyclicLeftApproximation n) ∧
    Asymptotics.IsEquivalent (Filter.atTop : Filter ℕ)
      (fun n => oppermannCyclicLeftApproximation n)
      (fun n => oppermannCyclicApproximation n) ∧
    Asymptotics.IsEquivalent (Filter.atTop : Filter ℕ)
      (fun n => (oppermannCyclicCountRight n : ℝ))
      (fun n => oppermannCyclicRightApproximation n) ∧
    Asymptotics.IsEquivalent (Filter.atTop : Filter ℕ)
      (fun n => oppermannCyclicRightApproximation n)
      (fun n => oppermannCyclicApproximation n)
Sources
  • J. E. Cohen, Conjectures about Primes and Cyclic Numbers, J. Integer Seq. 28 (2025), Article 25.4.1.
Uses 6
Statement usesCyclic numbers · Simplified approximation for cyclic numbers near squares · Cyclic numbers in the left Oppermann interval · Cyclic numbers in the right Oppermann interval · Left-hand approximation for cyclic numbers near squares · Right-hand approximation for cyclic numbers near squares

TheoremPower sums of cyclic numbers#●ready to prove

Let \(k \ge 1\) be an integer. Let \(c_n\) be the \(n\)-th cyclic number (\(c_1 = 1\)), let \(C(x)\) be the number of cyclic numbers \(m \le x\), and let \(\gamma\) be the Euler–Mascheroni constant. Then, as \(n \to \infty\) through the natural numbers,

\[ \sum_{i=1}^{n} c_i^k \sim \frac{n c_n^k}{k+1} \sim \frac{n^{k+1} e^{k\gamma} (\log \log \log n)^k}{k+1}, \]

and, as \(x \to \infty\) through the real numbers,

\[ \sum_{m \le x,\ m \text{ cyclic}} m^k \sim \frac{C(x)\, c_{C(x)}^k}{k+1} \sim \frac{C(x)\, x^k}{k+1} \sim \frac{x^{k+1}}{(k+1) e^{\gamma} \log \log \log x} \left(1 - \frac{\gamma}{\log \log \log x}\right). \]
MetaMathlibExt.sum_pow_cyclicNumbers_isEquivalent · 17 lines 
public theorem_wanted sum_pow_cyclicNumbers_isEquivalent (k : ℕ) (hk : 1 ≤ k) :
    let c : ℕ → ℝ := fun n => (Nat.nth IsCyclicNumber (n - 1) : ℝ)
    let γ := Real.eulerMascheroniConstant
    let C : ℝ → ℕ := fun x => ((Finset.Icc 1 ⌊x⌋₊).filter IsCyclicNumber).card
    IsEquivalent atTop (fun n : ℕ => ∑ i ∈ Finset.Icc 1 n, c i ^ k)
        (fun n : ℕ => n * c n ^ k / (k + 1)) ∧
    IsEquivalent atTop (fun n : ℕ => n * c n ^ k / (k + 1))
        (fun n : ℕ => (n : ℝ) ^ (k + 1) * Real.exp (k * γ) *
          Real.log (Real.log (Real.log n)) ^ k / (k + 1)) ∧
    IsEquivalent atTop
        (fun x : ℝ => ∑ m ∈ (Finset.Icc 1 ⌊x⌋₊).filter IsCyclicNumber, (m : ℝ) ^ k)
        (fun x : ℝ => C x * c (C x) ^ k / (k + 1)) ∧
    IsEquivalent atTop (fun x : ℝ => C x * c (C x) ^ k / (k + 1))
        (fun x : ℝ => C x * x ^ k / (k + 1)) ∧
    IsEquivalent atTop (fun x : ℝ => C x * x ^ k / (k + 1))
        (fun x : ℝ => x ^ (k + 1) / ((k + 1) * Real.exp γ * Real.log (Real.log (Real.log x))) *
          (1 - γ / Real.log (Real.log (Real.log x))))
Sources
  • Joel E. Cohen, Conjectures about Primes and Cyclic Numbers, Journal of Integer Sequences 28 (2025), Article 25.4.7, Theorem 1 (jis-2025-25.4.7-thm-1).
Uses 1
Statement usesCyclic numbers
6 fully proved9 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.