The Binary Totient Series

Integral relations.

Rational independence becomes an integral normal form because every omitted section is an integer multiple of a retained one. Keep the formal coefficient vectors separate from the sequences: a relation is nonzero in the former group and evaluates to zero in the latter. Fix $e\ge 1$, write $F_{j,r}(n)=\phi (2^{j}n+r)$, and let $I_e=\{(j,r):0\le j\le e,0\le r<2^j\}$. Retain $F_{0,0}$, $F_{1,0}$, and the odd-residue sections at levels $1,\dots ,e$; call this retained index set $J_e$. The totient identities reduce every omitted section to $F_i=a_i{F}_{j(i)}$ for a retained section $j(i)$ and an integer $a_i\ge 0$. Thus the retained family generates the lattice $L_e=\sum _{i\in I_e}\mathbb{Z}{F}_i$. Its rational independence gives integer independence as well: every element of $L_e$ has unique integer coordinates in these $2^e+1$ retained sections.

To describe all integral relations, let $E_i$ denote the formal coordinate vector in ${\mathbb{Z}}^{I_e}$ and use the evaluation map

For each omitted index put $R_i=E_i-a_i{E}_{j(i)}$. Then

For a vector $c$, subtract $\sum _{i\notin J_e}{c}_i{R}_i$. All omitted coordinates disappear, and the retained coordinate at $j$ is $c_j+\sum _{i\notin J_e,j(i)=j}{a}_i{c}_i$. The vector is a relation exactly when every retained coordinate is zero. In that case its relation coefficients are already known: they are the original omitted coordinates $c_i$. Uniqueness follows because $R_i$ has coefficient $1$ at its own omitted index and $0$ at every other one. These unit coefficients explain why no division, and no passage from $\mathbb{Q}$ back to $\mathbb{Z}$, is required. The depth-two base-six example in the short paper illustrates these two-term rows. The distinction between the retained basis and the redundant spanning family of all sections already matters for $k$-regular sequences that are not eventually zero: their growth exponent is the base-$k$ logarithm of the joint spectral radius of their section matrices in a basis, whereas a redundant spanning family gives only an upper bound (Coons [3]). The totient is not regular, so that theorem does not apply; the short paper records how the section maps act on the retained bases from one level to the next.

The integral normal form and the full dyadic rational basis are formally checked in Lean. The formal statement gives the same construction for every integer base $k\ge 2$, with relation rank $\sum _{j=1}^{e-1}{k}^j$. The full dyadic assembly separately gives a basis for the infinite rational span and for its finitely supported rational relations. These finite and infinite statements should not be confused with a claim about infinite sums of relations.

Relation to the series value. Infinite section rank does not imply irrationality of $S$. The result quantifies the nonregularity already cited above: it gives the rank, the retained sections and their integral relations. Martin’s simultaneous inequalities supply another proof for pairwise nonproportional affine forms with positive slopes [4]. His theorem does not separate $n$ from $2n$; the two evaluations above do that. The linked Lean proof is independent of Martin’s theorem.

The same independence argument also bounds the rank of an integral carry. If $S\in \mathbb{Q}$, choose an integer $v>0$ with $vS\in \mathbb{Z}$ and put $u_N=v{R}_N$, where $R_N=\sum _{j\ge 1}\phi (N+j)2^{-j}$. Then $u_N\in \mathbb{Z}$,

For every $e\ge 0$,

This is the finite family in the linked statement (not_irrational_totientSeries_implies_unbounded_carryRank_unconditional); it contains all carry residues at levels $1,\dots ,e$, not just odd residues or an unspecified retained subfamily. Indeed, for each odd $r$ with $0<r<2^j$, the recurrence gives

These $2^e-1$ totient sections are independent and belong to the span of the displayed carry sections after multiplication by $v\ne 0$. The rank bound follows. The boundary condition $u_N/2^N\to 0$ identifies the canonical carry, but is not used in this rank-transfer argument.

A contradiction would require an upper bound on the same carry rank. Rationality and the recurrence supply no such bound: Section 12.6 constructs a rational $5/4$ series whose unchanged odd totients force exactly this rank transfer. The changed even coefficients break other totient identities. Hence the comparison rules out a rank argument based only on rationality, linear growth and the recurrence, while leaving arguments using those additional identities untouched.

A separate finite-dimensional calculation concerns the matrix $U_N(i,j)=\mu ((i+1)/(j+1))$ when $(j+1)\mid (i+1)$ and zero otherwise, for $0\le i,j<N$. It is lower triangular with diagonal entries one. Hence $det{U}_N=1$ and the map $x\mapsto U_{N}x$ is injective (incidenceMobius_det_eq_one). This proves injectivity of that particular map, not the impossibility of every finite-dimensional argument for irrationality.

The evaluation-matrix argument. For functions $f_1,\dots ,f_s$ with values in a field, points $n_1,\dots ,n_s$ for which $det(f_j(n_i))\ne 0$ prove linear independence: evaluating a relation gives an invertible linear system for its coefficients. This elementary criterion is Proposition 6.24. It does not, by itself, construct the points. Here the totient formula, CRT and Dirichlet’s theorem provide them for nonproportional affine forms, followed by the separate zero-residue argument. Another arithmetic function would require its own argument for nonvanishing of the evaluation determinant.