Papers With

← All papers
First page of A counterexample to a subadditivity conjecture of Cohen for Sophie Germain cyclic numbers

A counterexample to a subadditivity conjecture of Cohen for Sophie Germain cyclic numbers

Josué Alexander Ibarra

math.NT Jul 9, 2026 · v1 math.CO
formalization number-theory
Read PDF arXiv abstract
TL;DR
A counterexample to Cohen's subadditivity conjecture for Sophie Germain cyclic numbers is formalized and kernel-verified in Lean 4 over Mathlib.
Abstract
An integer $n \ge 1$ is cyclic if $\gcd(n,\varphi(n))=1$ (equivalently, if every group of order $n$ is cyclic), and Sophie Germain cyclic if both $n$ and $2n+1$ are cyclic. Let $C_σ(N)$ count the Sophie Germain cyclic integers in $[1,N]$. Cohen conjectured that $C_σ$ is subadditive, $C_σ(m+n) \le C_σ(m)+C_σ(n)$ for all $1 \le m \le n$ (his Conjecture 66), having checked $m,n \le 10^6$ without finding a counterexample. We give one: at $m=31$, $n=3928$, $C_σ(3959)=697 > 696 = C_σ(31)+C_σ(3928)$. The argument is short, and is verified by the Lean 4 kernel.
Problem

Cohen conjectured (Conjecture 66) that the Sophie Germain cyclic counting function C_σ is subadditive, C_σ(m+n) ≤ C_σ(m)+C_σ(n), reporting no counterexample for m,n ≤ 10^6.

Approach

A window (3928,3959] of length 31 is shown to contain eleven Sophie Germain cyclic integers versus ten in [1,31]. Counts are computed with two independent totient implementations and cross-checked against Cohen's tabulated value. The negation of the conjecture is formalized in Lean 4 over Mathlib, defining cyclic via Nat.Coprime n (Nat.totient n) and C_σ via Nat.count, splitting the count at 3928 to avoid evaluating the cumulative total.

Results

At m=31, n=3928, C_σ(3959)=697 > 696 = C_σ(31)+C_σ(3928), disproving the conjecture. The Lean proof depends only on propext, Classical.choice, and Quot.sound, avoiding native_decide, so it is checked by the kernel.