The Binary Totient Series

Cancellation versus a certificate.

The first-harmonic implication converts the stated cosine bound on one block into a finite residue certificate (exists_certifiedKill_of_first_harmonic_gap). To prove irrationality, the bound must hold with the quantifiers in Section 3: for every shift and beyond every block threshold. A finite identity for the sum, or a computation at one block, does not establish this assertion.

Sign versus distance from an integer.

The positivity theorem for the LCM tail difference (actualLcmTailDiff_shift_pos) identifies the relevant endpoint under the stated size and modulus bounds. Nonintegrality follows only after excluding the corresponding residue interval (actualLcmTailDiff_notMem_int_of_topEdgeResidueGap). Likewise, the terminal-dominance condition is a sufficient hypothesis, not a construction of the required parameters (PowerTwoFlexibleActualTerminalDominanceSupply). Under integrality its inequality contradicts positivity of the terminal carry; the contradiction establishes sufficiency, not the inequality itself.

An error bound versus a separated approximation.

The finite-tail approximation has a uniform error radius (abs_actualLcmTailOrbit_sub_rawApprox_lt). The cited exact check supplies nonintegrality at the two exponents $a=4,6$ (actualLcmTailOrbit_four_and_six_notMem_int); it is not an assertion that no other exponent works. To obtain irrationality by this criterion, separation must occur at arbitrarily large LCM scales. In the nondivisor approximation of Section 6.6.8, the error bound is also proved when $D\ge 2H$. Its remaining requirement is finite rational separation, not an additional convergence hypothesis.

Denominator growth versus approximation quality.

The lower bound for the product of the upper-half Mersenne factors (upperHalfMersenneProduct_lower_bound) concerns a denominator expression. An irrationality argument needs a comparison with the error of the corresponding approximation. Growth of that denominator expression alone does not give either a successful residue test or a nonintegral totient tail.

A rank lower bound versus a contradiction.

The coefficient independence and hypothetical-carry rank bounds hold uniformly in the level (linearIndependent_canonicalTotientKernelFamily, not_irrational_totientSeries_implies_unbounded_carryRank_unconditional). A contradiction would require an upper bound for the actual carry that is strictly smaller than the lower bound at some level. The rational $5/4$ comparison disproves the proposed generic upper bound. The separate integer boundary conditions in the cited adjugate calculation are inconsistent (false_of_compressedAdjointCertificate), but that calculation does not exclude matrix arguments with different boundary conditions.

Quantifiers must be checked independently.

For example, a statement of the form $\mathrm{\exists }N\mathrm{\exists }L\mathrm{\forall }h$ does not provide the required $\mathrm{\forall }h\mathrm{\forall }{N}_0\mathrm{\exists }N\ge N_0\mathrm{\exists }L$. The first assertion controls many shifts at one location; the second requires arbitrarily late locations for each fixed shift. Relabelling a source statement does not bridge this difference.