Long paper
The Binary Totient Series
Summary. The dyadic totient sections through level
Start here, by the editorial route
In this paper
The exponential-sum criterion
We express the truncated tail difference as a phase and ask for cancellation when that phase is summed over a block. The following implications explain how a saving gives a residue certificate and, with the required quantifiers, Definition 1.2.
Definition 9.1 (The truncated difference). For
This is the depth-totientTail).
windowDiscrepancy
Definition 9.2 (The central-residue condition).
That is: the residue of certifiedKill_depth_floor).
certifiedKill
Definition 9.3 (The complex phase and its real part). Put
The real part of windowFirstExp_re),
and norm_windowFirstExp).
Thus windowFirstCos
windowFirstExp
Theorem 9.4 (A real-part bound gives a certificate).
For all
then
Theorem 9.5 (The same implication for a nonempty
subset). For any nonempty finite
then
Theorem 9.6 (A norm bound gives the real-part
criterion). The complex norm bound implies the real-part bound
(
This sufficient condition is unproved. Then
proved in full, with no
further gap, by chaining Theorem 9.6
Observation 9.7 (What remains unproved). The implications
above do not establish the cofinal block estimate. Three further Lean
statements retain a separation or gap hypothesis: one uses the
two-element set AdjacentPhaseSeparation.lean),
and the other two use a supplied finite set PivotAntiReconstruction.lean,
PivotAntiReconstruction.lean).
They prove what follows from the relevant estimate; they do not provide
that estimate at arbitrarily large scales. The finite numerical
observations in Table 1 are a different kind of
evidence and do not discharge this quantified hypothesis.
Remark 9.8 (What the reduction does and does not prove). The
required savings are explicit: a real-part bound of
The inequality
The subset theorem permits any nonempty finite sample inside
About this paper
Authorship and AI use. Will Cook built and directed the research infrastructure and maintains the public release. He reviewed claims when he could. AI agents did most of the research and drafting. Cook did not independently verify every claim.
Cite and contact. Cite this paper by its title, author and date above, with its PDF; cite the earlier sources it uses for a mathematical result. For software, use the release citation and give the commit used. Contact Will with questions or corrections.
Prefer the manuscript?
Equations typeset from the exact TeX. Rendered from the LaTeX manuscript source with file fingerprint sha256:2be13b340f9dafc4. Its file fingerprint matched the published source record, so the PDF above, the LaTeX, and this page are one manuscript. Redeploying the site regenerates this page from whatever the public repository holds at that moment.