The Binary Totient Series

The comparison with value $5/4$.

We alter only even coefficients, whose weights are $2^{-2m}=4^{-m}$. Thus we need a base-four expansion of $5/4-S$, with signed digits small enough to keep the corrected coefficients between zero and their indices. The digits $-2,-1,0,1$ will do this; the first even coefficient will require its own check. The elementary bounds $9/8\le S\le 3/2$ follow respectively from the first four terms and from $\phi (n)\le n-1$ for $n\ge 2$. Put $x_0=5/4-S$ and, for $m\ge 1$, define

The interval $[-2/3,1/3)$ contains $x_0$ and is preserved by this recurrence, so $d_m\in \{-2,-1,0,1\}$. Iteration gives

Consequently $x_0=\sum _{m\ge 1}{d}_m{4}^{-m}$. Define

These are nonnegative integers: for $m\ge 2$, $\phi (2m)\ge 2$; for $m=1$, the sharper bound $x_0\ge -1/4$ gives $d_1\ge -1$. The inequalities $d_m\le 1$ and $\phi (2m)\le 2m-1$ also give $c(n)\le n$. Thus $|c(n)-\phi (n)|\le 2$ and

This is the centred base-four construction in the Lean comparison-series theorem.

The construction has separated value from rank: the even coefficients set the value, while the unchanged odd coefficients force large rank. For the latter, take $v=4$ and $u_N=4\sum _{j\ge 1}c(N+j)2^{-j}$. The rational sum makes $u_N$ integral; the coefficient bound gives $0\le u_N\le 4(N+2)$. For odd $r$, the carry recurrence and $c(2^{j}n+r)=\phi (2^{j}n+r)$ give

The same $2^e-1$ independent totient sections therefore lie in the span of the carry sections at levels $1,\dots ,e$, proving ${\mathrm{rk}}_e(u)\ge 2^e-1$ for every $e\ge 0$. The corresponding formal statement is the unbounded-rank theorem for this comparison. This example is distinct from the bounded $3/2$ parity comparison in Proposition 1.9. It disproves an inference from the listed assumptions alone, not one that also uses identities of the actual totient coefficients.

The rank quantities.

Finite-dimensional span of all dyadic sections is the definition of a $2$-regular sequence in the sense of Allouche and Shallit [1]. For integer-valued sequences this is equivalent to finite generation of the $\mathbb{Z}$-module generated by the sections: if their span has dimension $d$, some $d$ evaluations embed it in ${\mathbb{Q}}^d$ and that module in ${\mathbb{Z}}^d$. Coons [2] proved that $\phi$ is not $k$-regular for any $k\ge 2$. The unconditional Lean theorem (Erdos249257.not_finiteDimensional_span_fullTotientKernel) proves the case $k=2$ independently. For integer coefficient and carry sequences, the recurrence transfers non-$2$-regularity of the coefficients to non-$2$-regularity of the carry. A proof must include the zero-residue sections, not just the positive residues. The following argument gives an explicit dimension bound.

For a rational-valued sequence $f$, let $V_e(f)$ be the span of all its sections through levels $0,\dots ,e$. Define the backward shift by $(Bf)(0)=0$ and $(Bf)(n)=f(n-1)$ for $n\ge 1$, and let ${\delta }_0$ be $1$ at $0$ and $0$ elsewhere. A level-$j$ section of $Bf$ is a section of $f$ if its residue is positive. At residue zero it is the backward shift of $n\mapsto f(2^{j}n+2^j-1)$. Hence

For integer sequences $c,u$ and a positive integer $v$, the recurrence $vc(n+1)=2u(n)-u(n+1)$ gives

Since every section of ${\delta }_0$ is $0$ or ${\delta }_0$, it follows that

In particular, bounded carry ranks would force bounded coefficient ranks. Non-$2$-regularity of $c$ therefore forces unbounded carry ranks. This is an ordinary proof, not a claim of a new Lean declaration. It also gives the generic bound ${\dim }_{\mathbb{Q}}{V}_e(u)\ge 2^{e-1}$ for $c=\phi$ and $e\ge 1$, using the coefficient rank $2^e+1$. The factor $2$ is not an additive $O(1)$ loss, and this bound concerns all sections, including level zero.

The theorem for $\phi$ in Proposition 1.6 is sharper: the carry sections at all residues of levels $1,\dots ,e$ have rank at least $2^e-1$. It uses the independence of the odd-residue totient sections. Neither lower bound is an irrationality proof, since rational coefficient series can have nonregular carries. The separate $5/4$ comparison verifies this directly. Any proposed rank upper bound must use additional totient-specific hypotheses not satisfied by the $5/4$ comparison sequence.