Back to all results
certificate C-0042

The sharp full-range Rosser--Schoenfeld product and totient coefficients

Two classical full-range inequalities have exact coefficients within their original formula shapes. For the Mertens prime product on $x\geq286$, the normalized maximum occurs uniquely at $x=286$. For $n/\varphi(n)$ on $n\geq3$, the normalized maximum occurs uniquely at the exceptional primorial $N_9=223092870$.

\[C_{\rm prod}=0.482761856265219\ldots,\qquad C_{\varphi}=2.506369279696429\ldots\]
Download PDF LaTeX source Verifier bundle

The two statements

Let $P(x)=\prod_{p\leq x}p/(p-1)$. The first result determines the least coefficient in the Rosser--Schoenfeld product bound on the unchanged range $x\geq286$.

The second result determines the least coefficient in their global totient formula for integers $n\geq3$.

\[P(x)\leq e^\gamma\log x\left(1+\frac{C_{\rm prod}}{\log^2x}\right)\qquad(x\geq286)\]
\[\frac n{\varphi(n)}\leq e^\gamma\log\log n+\frac{C_\varphi}{\log\log n}\qquad(n\geq3)\]

Product normalization

The product inequality is normalized so that its coefficient is the maximum of a stepwise-smooth function. Since no prime lies between $283$ and $293$, the candidate at $x=286$ uses the Euler product through $283$.

On an interval with no prime, the product is constant. The derivative test shows that the normalized error decreases between successive prime jumps, reducing the finite problem to the endpoint and values immediately after primes.

\[E(x)=\log x\left(e^{-\gamma}P(x)-\log x\right)\]
\[C_{\rm prod}=E(286)=\log286\left(e^{-\gamma}\prod_{p\leq283}\frac p{p-1}-\log286\right)\]
\[E'(x)=\frac{e^{-\gamma}P(x)-2\log x}{x}<0\]

Product maximum and tail

Every later prime jump through the Dusart handoff is strictly below $E(286)$. The nearest competitor is $p=293$, separated by more than $0.0236028$.

Dusart's product estimate gives a normalized tail at most $1/(5\log x)$. At the handoff this is below $0.014$, far below the candidate, so $x=286$ is the unique global maximizer on the stated range.

\[C_{\rm prod}=0.482761856265219690669858626593363196\ldots\]
\[P(x)\leq e^\gamma\log x\left(1+\frac1{5\log^3x}\right)\qquad(x\geq2\,278\,382)\]

Totient exceptional value

Rosser and Schoenfeld proved the stronger coefficient $5/2$ for every $n\geq3$ except one integer. That exception is the product of the first nine primes.

Evaluating the normalized error at this primorial gives a value strictly between $5/2$ and the published exception-covering decimal $2.50637$. Since every other integer has normalized error below $5/2$, the exceptional primorial is the unique global maximizer.

\[N_9=2\cdot3\cdot5\cdot7\cdot11\cdot13\cdot17\cdot19\cdot23=223092870\]
\[C_\varphi=\log\log N_9\left(\frac{N_9}{\varphi(N_9)}-e^\gamma\log\log N_9\right)\]
\[C_\varphi=2.506369279696429677313820930790467588\ldots\]

Certificate role

For the product result, the pinned certificate enumerates all $168064$ primes through the handoff, checks negative derivative on every prime-free interval, compares every later jump, and verifies the analytic tail margin.

For the totient result, it constructs the exceptional primorial exactly, evaluates its Euler ratio and logarithms with directed Arb arithmetic, and certifies both the sharp value and the strict decimal rounding $C_\varphi<2.50636928<2.50637$. The conclusion for all other integers uses the cited $5/2$ theorem.

\[C_{\rm prod}<0.482762<\frac12\]
\[\frac52<C_\varphi<2.50636928<2.50637\]

Pinned certificate

The pinned Arb certificate proves the product endpoint is the unique finite prime-jump maximum and lies above the Dusart tail, then evaluates the unique Rosser--Schoenfeld totient exception and its strict roundings. The all-other-n totient step is supplied by the cited theorem.

uv run --frozen python canon/witnesses/C-0042/verify.py
  • canon/witnesses/C-0042/verify.py
  • canon/witnesses/C-0042/PIN.md

Scope

Both coefficients are exact for the displayed Rosser--Schoenfeld product and totient formulas on their original ranges.

Sources

  • Canonical claimcanon/claims/C-0042-sharp-rosser-schoenfeld-product-totient-coefficients.md
  • Pinned certificate notecanon/witnesses/C-0042/PIN.md
  • Certificate sourceexperiments/mertens_product_rs_sharp_coefficient/verify.py