The Binary Totient Series

Further background.

Erick Wong posted a proof that $\sum _{n\ge 1}(\phi (n)modk)k^{-n}$ is irrational for every integer $k>2$ on Mathematics Stack Exchange on 29 March 2015 [5]; there the base equals the modulus. Erdős’s 1957 criterion already gives every base (Remark 1.13). The Möbius-square form of $S$ and its coprimality interpretation were posted publicly before this record, as credited in §5.4. Kovač and Tao show that suitable subsums of Lambert series in distinct integer bases can be rational [18]; the freedom to choose those subsums is absent for $S$. The Lambert-series factorisations of Merca [17] and of Merca and Schmidt [16] are transform background for the Möbius–Mersenne coordinate. Balasubramanian, Giri and Srivastav prove asymptotics for finite shifted convolutions of divisor-convolution functions, including $\phi (n)/n$, uniformly for $|h|\le x/2$ at cutoff $x$ [19]. Their partial-summation extension uses differentiable weights with bounded derivative on the summation interval [19]. Applying that observation here would require control of the weighted error for the present phases; no such estimate is established in this record. In the totient specialisation the divisor-convolution kernel is $\mu (d)/d$ and both decay exponents in their theorem are $1$, giving an $O({\log }^{2}x)$ error for the two-point product. The present quantity is instead an exponential of a window of overlapping totient values, with a denominator growing with $L$. Partial summation would carry the variation of its weight into the error term; it does not remove the need to bound that variation and the resulting weighted error. The cited results are not themselves the dyadic residue separation required by $\mathrm{Sep}$. The remaining sources are cited where their hypotheses are used.

At the generating-function level, the published height criterion of Adamczewski, Bell and Smertnig gives $k$-regularity for a $k$-Mahler series with integer coefficients of polynomial growth  [35]. For the totient coefficients the logarithmic heights are $\log max(1,\phi (n))\le \log n$ for $n\ge 1$, so Coons’s nonregularity already rules out $k$-Mahler equations in every base. The later multiplicative classification of Bell and Smertnig provides another route [32]. The algebraic and $D$-finite classifications of Bell, Bruin and Coons belong to the same function-level context [33]. They do not by themselves decide the value at $z=1/2$.

Automatic prime-sampling theorems address a different issue. Adamczewski, Drmota and Müllner identify a computable local coprimality condition governing the relevant logarithmic densities, with a conditional ordinary-density transfer [34]. Their theorem does not assert that every output state has positive density on a prescribed prime progression, nor does it prove independence with automatic coefficient weights. Any use for that purpose needs its own compatibility argument.

Sources and data.

The evidence record lists every Lean declaration, version and check behind the margin marks.

Verification scope.

Kernel checking validates a formal proof of its stated proposition relative to the declared axioms. It does not check that every prose summary has the same hypotheses or verify the literature comparisons. In particular, a checked implication with an unproved hypothesis is not a proof that Problem 249 is solved.

Funding and competing interests.

This work received no external funding. The author declares no competing interests.