The Binary Totient Series

Verification and reproducibility

The links below identify formal declarations at the supplied source revisions. A checked conditional implication retains its hypothesis; the linked source alone does not establish that input for $\phi$. The record gives the available Lean and Comparator status and does not report a new replay or independent review of the printed proofs.

Bases and relations.

reduction of sections with residue zero; reduction of even residues; independence; span equality; basis; independence; dimension; the exact finite-truncation rank; infinite-dimensionality directly; coordinate specification; injective residues; unique representation; level count; section-index count; index as two plus the odd-residue count; full index count; a nonzero evaluation determinant; an invertible minor for affine totient sections; power-multiplication identity; affine cross-gcd identity; nonzero reduction scalar; all-base residue step; canonical spanning; span equality; rank in every base from independence; all-base truncation rank from independence; independence in every integer base; the rank of the retained all-base family; the rank of all sections through a finite level.

Tail identities, residue tests and carries.

the finite-prefix and tail identity; definition; certificates for shifts 1 through 8; nonintegral tail differences at the checked shifts; the integer carry recurrence and its growth bound; residue recurrence; comparison of the two residue conditions; exact equivalence; a certificate in each sufficiently late pair of multipliers; pointwise equivalence; global equivalence; equivalence after setting depth equal to the shift; irrationality and arbitrarily large certificates; the carry-rank lower bound under rationality; carry rank at least $2^e-1$ from independent totient sections; modular periodicity and the rank lower bound for the same carry; forcing vanishing; geometric reduction; identity; sign; primes; prime powers; unboundedness; exact centre decomposition; explicit error bound; separation criterion; target equivalence; endpoint nonnegativity; foreign-channel identity; five-point loss bound; simultaneous finite family; finite horizon; vanishing block; nonzero block; centrality equivalence; equivalence of the two conditions; conditional irrationality theorem; finite complement bound; exact channel split; conditional target-miss theorem; the periodic theorem; $\sum \phi (n)/(2^n-1)=2$; rationality and integer carries with controlled growth; diagonal split; definition; definition of the scaled tail; the proposed cyclotomic residue condition; the checked equivalence; checked conditional support/period counterexample; the checked binary-layer theorem; certificates with depth equal to the period multiple.

Finite denominator exclusions.

exclusion; reduced-denominator form; first failure; the conditional implication; farey gap; the denominator bound at window 240; denominator exclusion from a finite interval; the earlier denominator bound at window 120; denominator exclusion for the coprimality probability; list; verification; certificates at every scale through 82.

Least common multiples and limits of the tested methods.

certificate completeness; tail-difference integrality; irrationality iff every tail difference is nonintegral; exact frontier; forward implication; positive tail differences; negative endpoint representative; residue near the upper endpoint; divisibility preserved by finite combinations of shifts; the counterexample with sparse prescribed values; pointwise; cofinal at each shift; $\mathrm{lcm}$ diagonal; the certificate at $t=2^4$ and depth $23$; the certificate at $t=2^6$ and depth $93$; actual-orbit non-integrality at both heights; certificates beyond every threshold $a_0\le 6$; an explicit approximation error; the approximation as an integer over $4^q$; distance at least $1/32$ from every integer; the cofinal separation hypothesis; the conditional endpoint theorem; the staircase is impossible under the stated room hypothesis; terminal-remainder identity; the limitation of fixed-precision valuation data; rationality from an integral tail difference.

Möbius identities and rational approximation.

unique minimizer; uniform lower bound $21/320$; lower bound $1/16$; $1/15$ failure; positive weighted averages of the quotients; rational linear-form obstruction; divisor-count layer; first gcd moment; no fixed index; the primorial divisibility; irrationality of the Erdős–Borwein series; $\sum \mu (n)/(2^n-1)=1/2$; the squared-Mersenne expression for the totient series; the coprimality-probability expression; the Lambert-weighted sum over coprime positive pairs; the Stern–Brocot recursion with stopping; $s=1$; $s=2$; first difference; second difference.

Proposed exponential-sum and prime-factor estimates.

window-separated pairs; the unproved quantitative separation condition at primes; a positive adaptive truncation budget; $S$ is irrational; density hypothesis; block-gap hypothesis; density-to-gap implication; exact squaring recurrence; iterate formula; initial-phase normal form; initial-phase equivalence; dyadic-root obstruction; prime-alignment implication; mixed difference; separable case; fixed-stencil uniqueness; a four-point divisor-layer identity; a centred representative for a residue class modulo an even modulus; eventual nontriviality and coprimality of the layers; order divisibility with bounded extension degree; exclusion of any fixed finite prime support; unbounded prime divisors; membership; injectivity; image equality; checked counterexample; the exact decomposition into four prime-factor contributions; the conditional irrationality theorem; the four inequalities on a common block; the first-harmonic bound from those four inequalities.