Organisation
The argument starts from
What finite calculation can refute that integrality? The residue test in Definition 1.2 encloses the tail difference in an explicit error interval. Section 5 gives the identities and the independent Farey-window exclusion. Appendix A supplies the complete propagation, Mersenne-residue and rank-one arguments cited in the short paper.
Which information is insufficient to supply such
calculations? The short
paper determines all finite-level totient relations, with a basis of
What additional estimate would suffice? Section 3 gives the quantified conditions. Section 12.3 separates the weighted exponential-sum estimate from the counting and group-mean bounds, corresponding to the four-estimate problem in the short paper. A second sufficient condition estimates only the average over good indices and needs no group-mean input. Appendix B records the formal declarations; an implication proved there does not establish its remaining hypothesis.
Totient sections and tail differences
Put
The coefficient relations are finite linear identities. The series question asks whether a particular infinite weighted sum can be rational. Put
The series converges
absolutely because
Throughout, a cofinal condition means that a witness exists beyond each threshold. It need not hold at every sufficiently large index. Each comparison sequence is used only for the properties it preserves; agreement with a fixed totient prefix, for example, imposes no multiplicativity condition on the continuation.
Remark 1.1 (Earlier coefficient results). Erdős and Graham
record the irrationality question for
To test rationality, we remove the finite prefix, which becomes an
integer after multiplication by Erdos249257.TotientTailPeriodKiller.totientTail,
two_pow_mul_totient_series_eq).
If Erdos249257.TotientTailPeriodKiller.eventual_period_of_not_irrational).
Indeed,
and the right side is integral for those choices.
Thus it suffices, for every positive shift
the
depth-
a decidable condition (Erdos249257.TotientTailPeriodKiller.windowDiscrepancy,
Erdos249257.TotientTailPeriodKiller.certifiedKill).
The omitted tails satisfy the exact identity
Both tails are nonnegative, so their difference is bounded in absolute
value by the larger bound Erdos249257.TotientTailPeriodKiller.exists_certifiedKill_iff_tail_diff_notMem_int).
The resulting quantified condition is the following.
Definition 1.2 (The quantified residue condition).
irrational_totient_series_iff_certificate_supply).
The equivalence identifies the missing quantified input; it supplies no
certificate by itself.
One successful Erdos249257.TotientTailPeriodKiller.certifiedKill_depth_floor
Unconditional results
The finite denominator exclusion, the ranks of the totient sections and the tail-positivity statements below require no additional arithmetic hypothesis. To distinguish their conclusions, note that positivity excludes a zero tail difference, whereas irrationality requires a nonintegral one. The rank calculation concerns the coefficients and supplies neither conclusion about the value by itself.
Theorem 1.3 (Denominator exclusion from a fixed Farey
window). If
Equivalently,
This is obtained from a classical Stern–Brocot gap lemma (farey_gap)
applied at window
Proposition 1.4 (Finite certificate computations).
decide; and eight further period
examples at
Proposition 1.5 (Positivity does not exclude an
integer). Put
This needs no
irrationality hypothesis. If this difference is an integer and
then
lies strictly
between
For the next two propositions, a rational value
Here
Proposition 1.6 (Rationality forces unbounded carry
rank). If
Proposition 1.7 (Periodicity modulo an integer does
not bound rational rank). If
The rank and periodicity assertions hold together. This conditional
theorem alone is not a counterexample to a general periodicity-to-rank
implication: its antecedent is not established. The rational comparison
sequence with sum
Proposition 1.8 (Equivalent certificate conditions).
Put
also gives equivalent
quantified conditions, including its restriction to
Proposition 1.9 (A rational sequence preserving size
bounds, parity and aperiodicity). There is
These propositions separate several logical obligations. Positivity
leaves an upper-endpoint condition; a large rational carry rank is not a
contradiction; and exact equivalences still require a quantified
certificate condition. The stated size bounds, parity and aperiodicity
also hold for a rational comparison series. Each conclusion concerns its
stated hypotheses, not all possible arithmetic information about
Reduced coefficients
Reduction modulo
Proposition 1.10 (Residue series in every integer
base). Let
For every
, is irrational (radix_residue_series_irrational).For
and , the series is rational exactly when is constant on the even residue classes, and its value is then (rational_zmod_radix_observable_iff,positiveRadixValue_eq_of_even_constant).
Proof. For coefficients bounded by
For example, in base
Proposition 1.11 (Finitely many dilations). Let
For every
, the numbers and , , are linearly independent over (linearIndependent_one_and_least_residue_values).Let
be a finite set of positive integers, and for let and . For every , the numberis rational exactly when every
is constant on the even residue classes (rational_mixed_moduli_with_constant_iff).
Proof. (a) A relation gives integers
Given
The inverse
exists because
(b) Each
Remark 1.12 (Slowly growing dyadic moduli). Let
Proof. If
Remark 1.13 (Earlier results and the reduced coefficients).
Proposition 1.10(a), and with it
the first assertion of the short paper’s residue theorem, already
follows from Erdős’s Lemma 1 of [6]: if integers
Rational comparison sequences
Rational series can agree with the totient series on a fixed prefix, on parity at every index, or on specified linear data. The following constructions keep these requirements separate. Each gives a rational comparison satisfying the data named in its statement, and thus identifies what those data alone leave undetermined. The properties in different rows below belong to different constructions; they must not be combined into one comparison theorem.
| Construction | Data kept while the value is rational |
| Prescribed prefix (Theorem 2.4) | Any fixed totient prefix and the bound
|
| Parity (Proposition 1.9) | Parity at every index, aperiodicity and the stated size bound. |
| Value |
Every odd totient, changes of at most
|
| Signed interpolation (Section 10.10) | A prefix, all odd totients, and the specified moment and analytic data; not the full radial germ or all arithmetic identities. |
Finite data and rational continuations
We begin with a rational continuation of an arbitrary finite prefix (Theorem 2.4). Proposition 1.9 instead preserves parity at every index, a linear size bound and aperiodicity. The carry and linear descriptions in Propositions 2.11 and 2.12 impose different requirements again. Their counterexamples concern the displayed descriptions only; they do not exclude all finite-state or finite-dimensional arguments.
Two other limitations do not require a rational comparison sequence. A congruence construction can increase the index so much that its tail error exceeds the residue it produces (Proposition 2.9). An exact reformulation or a finite list of examples still needs the quantified arithmetic assertion (Proposition 2.7).
The finite certificates in Proposition 1.4 and the
A rational sequence with any prescribed totient prefix
A finite prefix leaves the remaining coefficients free. We construct
a rational continuation satisfying the same linear size bound, then show
why it cannot satisfy the quantified residue condition. First we record
the two tail facts needed for a general coefficient sequence. For
Lemma 2.1 (A residue certificate excludes an integral
tail difference). Let
Proof. Splitting both tails after
Both tails on the right are
nonnegative, and Erdos249257.TotientTailPeriodKiller.tail_after_le
and used there to prove Erdos249257.TotientTailPeriodKiller.tail_diff_notMem_int_of_certifiedKill.
If
Lemma 2.2 (Generic tail-period law). Let
Proof. Since
The right side is integral because
Remark 2.3. Lemmas 2.1 and 2.2 are also checked for
every coefficient sequence satisfying
Theorem 2.4 (A rational sequence agreeing with any
finite totient prefix). Let
Then:
for all , so lies in the same coefficient class as ; for every , and consequently for every with ; , and the odd part of its reduced denominator is exactly ; is false; indeed it fails already at .
Hence for every
Proof. (i) is immediate; (ii) holds because
The first two terms have denominator
dividing
Corollary 2.5 (The limit of a finite-prefix
argument). No proof rule uniform over all
Remark 2.6 (Four distinct finite restrictions). Theorem 2.4 concerns the information
in a finite prefix. It does not identify
Proposition 1.9 gives another rational comparison sequence, this time preserving parity and specified aperiodicity properties. The two examples test different assumptions and must not be combined into a single stronger example.
Limits of specific reductions and estimates
We test several proposed deductions by retaining their assumptions and changing the conclusion. The constructions concern specified congruences, recurrences or estimates, so their force is limited to the corresponding deductions.
Proposition 2.7 (Three particular equivalences).
Certificate completeness. The complete residue tests considered here are equivalent to the corresponding nonintegrality assertions. Rewriting the quantified condition using one of these equivalences does not weaken it.
A selectable two-point sample. The condition is as follows. For every
and , choose with and , a nonempty set , a set of ordered pairs, and a real number . With , requireThis condition is equivalent to irrationality. For the converse, irrationality and the doubling map allow
and at arbitrarily large , with . The numerical requirement is then . The freedom to select matters: this is not an estimate on a sample prescribed in advance, such as all prime positions.Four integral tail differences. For
and positive integers , the conjunctionis equivalent to
alone. The affine transport identity for preserves integrality, so the three additional conditions add no restriction. Neither nor need be prime.
These three equivalences explain why these particular reformulations retain the original arithmetic question. They do not rule out useful weaker intermediate lemmas. The full-block and fixed-margin conditions in §3 ask for additional quantitative information that the three arguments above do not supply.
Remark 2.8. Second-difference certificates need not occur at
a smaller depth than first-difference certificates. At
Separately, unbounded growth of the denominator exclusions produced by the Farey windows would imply irrationality. The record does not establish a converse for that specific sequence of windows, so the proposed growth condition is used only as a sufficient condition.
Proposition 2.9 (Failure of a specified two-adic
congruence construction). A certificate requires the residue to lie
farther than
Remark 2.10 (Two further prescribed patterns). Two related
results concern particular prescribed patterns. Under the stated size
condition, the complete terminal divisibility pattern is impossible: its
last totient difference would be positive, below a modulus, and
divisible by that modulus (Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.not_actualLcmTerminalDyadicStaircase_of_room).
For the pattern with the last condition removed, the penultimate
difference is forced to be
A different sufficient condition would prescribe the accumulated sum
rather than an individual difference:
Proposition 2.11 (Information lost by specific carry descriptions).
Fix
and write . For , let vanish except at and . Each sequence satisfies , has the same binary sum , and has the same coefficients and scaled tails before position . Its scaled tail at position is . The common history therefore does not determine that tail. A finite set of labels that determines the tail for each member of this family must contain at least elements, one for each value of .Reduction modulo
forgets the initial value after the same recurrence steps: two affine binary orbits with different seeds satisfy , so the endpoint residue mod is independent of the initial carry.Fix a precision
, a finite list of nonnegative valuations and odd integers , and an initial integer . There are integers such thatAt each step, choose the centred representative of
modulo . The unrestricted integers are essential: the assertion does not prescribe the full coefficients .
These statements exclude decoders using only the specified common history, distinctions using only the endpoint residue, and contradictions using only the stated local symbols. They do not prove that the actual totient expansion cannot be studied by automata. A proposed application must verify that it uses no additional arithmetic information that the comparison families fail to preserve.
Proposition 2.12 (Four limits of particular linear constructions). The following four constructions have different limitations. They must not be read as a claim that every finite family of totient sections is independent: the full family has the explicit relations described in the short paper.
Dyadic sections and an integer identity. The retained family of
dyadic sections is linearly independent over for (Proposition 1.6). Separately, positive integers and integers cannot satisfybecause
gives . This elementary incompatibility concerns the displayed requirements; it does not exclude every argument using an adjugate matrix.Möbius incidence.
when and otherwise is lower triangular with unit diagonal, so for every . Hence multiplication by is injective; the corresponding coefficient transformation cannot create a nonzero vector in its kernel.Adjugate reconstruction. Let
and be finite families with . Reconstructing each value from two tails and bounding them separately gives the error bound . It is at least , sinceConsequently this particular bound cannot be less than
, whatever the size of the evaluation matrix.Finite combinations of shifts. The synthetic sequence in Observation 6.115 has the prescribed differences
for , where . It is of the form , and every finite integer combination of its shifts has the same form with a correspondingly shifted state. Thus these linear operations alone do not remove the compatible carry recurrence. Their uniform bounds depend on the absolute coefficient sum, as made explicit in that observation. The construction does not assert that equals the actual totient difference at other indices.
A further limitation concerns quotients of the finite sums
The proof bounds each infinite sum
Proposition 2.13 (The coefficient properties of the
rational example). The rational sequence in Proposition 1.9 satisfies uniform
boundedness,
Consequences of the comparisons
The residue margin and the truncation error must be controlled together. Enlarging a congruence may enlarge both, while a finite prefix constrains no later coefficients. Periodicity modulo an integer likewise places no general upper bound on rational rank. These comparisons leave the equivalent residue conditions intact, with their original requirements for witnesses at unbounded indices.
These are limitations of specified arguments, not an exhaustive classification of possible methods. In particular, an averaging estimate is one possible source of the missing information, not the only possible source. A new arithmetic identity or a propagation theorem could also be useful. The next section describes the precise assumptions of several approaches considered here.
Conditions that would imply irrationality
Below are quantitative sufficient conditions, an equivalent residue formulation, and a proposed generic rank bound. The rank bound is false, as its rational counterexample shows. The other arithmetic conditions remain open for the totient; the proofs establish their stated implications. They are examples of possible approaches, not an exhaustive list.
Cancellation on a full block
If every window residue lies close to an endpoint, its complex phase
lies close to
Definition 3.1 (The full-block norm condition). Write
It implies Erdos249257.TotientTailPeriodKiller.DTWFirstHarmonicNormGap
Erdos249257.TotientTailPeriodKiller.irrational_totient_series_of_first_harmonic_norm_gap
A bound on the real part also suffices: it is enough that Erdos249257.TotientTailPeriodKiller.exists_certifiedKill_of_first_harmonic_gap;
for the implication from Erdos249257.TotientTailPeriodKiller.exists_certifiedKill_of_first_harmonic_norm_gap).
Unpacked, the required object is a constant-saving cancellation estimate
for the dyadically weighted totient-difference exponential sum
No
theorem in this record establishes this estimate with the required
quantifiers. The displayed size inequality imposes a lower bound on
Comparison with the preceding counterexamples.
The earlier counterexamples do not establish or refute this block estimate. The following distinctions explain why those particular arguments do not settle it.
The parameters grow. The size condition forces the truncation depth to increase with
, so this is not a test of a fixed prefix.The sample is prescribed: all
are summed at one depth. Choosing two favourable indices does not establish this block estimate.The sum uses the accumulated totient differences. It does not prescribe individual values through a congruence construction.
The estimate concerns the actual phases. Neither a bound on carry rank nor agreement only in parity gives it.
The proved implication uses the real-part threshold
and the constant in the size bound . The stronger norm bound implies that real-part bound. These constants do not assert any distribution theorem for the totient phases.
Formal sources for these implications: Erdos249257.TotientTailPeriodKiller.windowFirstCos_gt_of_not_certifiedKill
Erdos249257.TotientTailPeriodKiller.exists_certifiedKill_of_first_harmonic_gap_subset
Remark 3.2 (The finite-prefix example does not choose a
method). The finite-prefix example does not select an analytic method.
It shows only that a proof valid for every sequence
Remark 3.3 (Finite certificate observations). In the
historical table of
A four-term bound for the real part
We isolate the phase of one term
Fix
Write
Since
Both factors have absolute
value
This follows by partitioning the indices and
using
Definition 3.4 (Four simultaneous inequalities). For
every
It implies Erdos249257.TotientTailPeriodKiller.DTWPivotResidualDecorrelation
Erdos249257.TotientTailPeriodKiller.irrational_totient_series_of_pivotResidualDecorrelation
First fix
The decomposition is an exact identity, proved in Lean (Erdos249257.TotientTailPeriodKiller.windowFirstExp_sum_eq_pivot_decomposition),
as is the implication from the four bounds to the real-part bound (Erdos249257.TotientTailPeriodKiller.first_harmonic_gap_of_pivotBudgetAt).
The reason a new estimate is needed is visible within one group:
The unweighted mean
vanishes while the weighted terms agree exactly. This example explains
why an implication is missing; it is not a counterexample to the
estimate for the actual totient windows. For the latter, only the
real-part bound Erdos249257.TotientTailPeriodKiller.mem_pivotFiber_one_overlap_iff),
using
The four inequalities have not been established together.
Propositions 12.6
and 12.7 give the
unassigned and excluded-cofactor bounds at minimal admissible depth. At
A nonzero determinant alone does not prove the needed correlation
estimate. The comparison in the linked source (Erdos249257.ResidualGaugeObstruction.locked_reconstruction_preserves_nonzero_minor)
preserves such a determinant while fixing an entire row of weighted
phases to
One bound on the good indices
Two counting estimates allow us to restrict the cancellation question
to
Theorem 3.5 (Irrationality from one bound on the good indices).
Suppose that for every
and every there are , with and a nonempty finite set of integers in withTake
, and . Suppose that for every there are arbitrarily large with
Proof. (a) At a depth satisfying the size inequality, a
nonempty set of indices below Erdos249257.TotientTailPeriodKiller.exists_certifiedKill_of_first_harmonic_gap_subset).
The hypothesis therefore supplies, for every
(b) For all large eventually_card_pivotGoodBases_gt).
Since
The trivial bound for the sum in (b) is
When the first two inequalities of Definition 3.4 hold with fiberMean_le_of_primeNumberTheorem).
Since dtw_of_fiberMean_and_centered,
irrational_totient_series_of_primeNumberTheorem_and_goodBase_gap).
Theorem 3.5(b)
supersedes that route. It assumes neither the prime number theorem nor a
bound on the group means, and asks only for
For clarity, the two sufficient estimates have different uses. The
centred route controls all four pieces and so bounds the sum on the
whole block. The
There is also a useful distinction between eventual and cofinal
hypotheses. At
A fixed separation at prime positions
Instead of averaging over a block, one may ask for a fixed gap at prime positions. The lower bound on the prime ensures that the corresponding tail indices lie beyond the required threshold.
Definition 3.6 (A fixed gap at prime positions). For
every DTWNaturalPrimeTailOrbitStrictGap
irrational_totient_series_of_naturalPrimeTailOrbitStrictGap
This asks for more than nonintegrality. A nonintegral real number can
be arbitrarily close to an integer, whereas the displayed condition
requires a fixed positive distance, along prime positions and for each
shift
Certificates with depth equal to the shift
The shift and truncation depth can be required to agree, provided the
shift is allowed to run through positive multiples of a fixed
Definition 3.7 (Depth equal to a shift multiple). For
every
It is equivalent to ApFullDepthEscape
apFullDepthEscape_iff_irrational
For a fixed pair apFullDepthEscape_iff_irrational).
The finite examples verify the starting hypothesis for individual pairs,
not for every
Formal sources: windowDiscrepancy_self_eq_totientBlock_sub
A false generic rank bound
The coefficient rank might suggest a bound on carries under rationality. The next proposed assertion makes that suggestion precise; the rational comparison following it disproves both versions.
Definition 3.8 (A counterfactual rank criterion). The
proposed assertion is a constant
Specifically, the proposed bound is
The alternative replaces
Both assertions in Definition 3.8 are false. The
comparison sequence with sum
Periodicity modulo
Guide to the detailed statements
The remainder records the formulas and proofs behind the preceding arguments. To use a statement, distinguish its conclusion from its input. A finite certificate excludes a family of denominators; a cofinal supply excludes every rational value. Positivity of a tail difference is not nonintegrality, and a conditional implication still needs its arithmetic premise.
The following entry points answer different questions; they are not successive steps of one proof of irrationality.
| Question | Where to read |
| Which section identities hold? | Section 10.8: independent sections and integral relations. |
| What does a finite computation exclude? | Section 5: tail residues; Section 5.3: the denominator cutoff. |
| Can one nonintegral difference yield more certificates? | Appendix A.1: propagation with growing shift and depth. |
| Which data still allow a rational value? | Section 2: comparison sequences, with their hypotheses kept separate. |
| Which estimate would suffice? | Section 12.3: the four-term decomposition; Theorem 3.5: the weaker good-index condition. |
| What was formally checked? | Appendix B: the declaration and source-version guide. |
The detailed statements retain their source references so that a proof can be recovered without treating a source label as another hypothesis.
Series identities and finite exclusions
The prefix-tail identity supports two different finite exclusions.
Residue certificates test a tail difference modulo
The series
We begin with the value and the prefix-tail decomposition used by all the subsequent tests.
Definition 5.1 (The Erdős–249 constant). Let
the two forms coinciding because
Remark 5.2 (Status). No proof or disproof of
The tail-shift identity
Multiplying by a power of two makes the finite prefix integral and
leaves a scaled tail. The tail values themselves may grow; it is their
classes modulo
Proposition 5.3 (Digit-shift identity). For
every
where
Consequence for rationality. Subtracting the prefix
identities at
If eventual_period_of_not_irrational).
Conversely, an integral difference for even one
The finite denominator bound
An interval containing
Lemma 5.4 (Farey gap, fully general). For
integers
Indeed, the two strict inequalities make
using
Proposition 5.5 (The Farey certificate at
For every
This bound is
sharp:
Here “failing” means that this particular enclosure can no longer
exclude the denominator. It does not mean that the mediant equals
Theorem 5.6 (Denominator exclusion). For every
Equivalently: if
Remark 5.7 (What this does and does not say). Theorem 5.6 is a complete,
unconditional finite fact: no rational of denominator at most
Equivalent expressions and their denominator bounds
The finite bound in Theorem 5.6 also applies to
the two expressions for
Proposition 5.9 (Fair-coin coprimality form).
Let
Equivalently, on the visible lattice: summing
Proposition 5.10 (The gcd-layer normalisation).
For independent fair-coin waiting times as above,
Theorem 5.11 (Denominator exclusion for the coprimality-probability form). Let
For
every
Theorem 5.12 (Denominator exclusion for the
Möbius-square form). With
Remark 5.13 (Why the bound halves, and why this is not new
information).
The Möbius-weighted identity
Subtracting
Proposition 5.14 (Möbius-square reduction).
where
Remark 5.15 (Why the bounded coefficients matter; the
Erdős-1948 regime). The identity of Proposition 5.14 rewrites
Combining this identity with irrational_erdosBorwein_series).
In contrast, the coefficients of the original power series satisfy
irrational_of_int_mul_near_int
and its base-power specialisation irrational_of_pow_mul_near_int)
applies to either representation if its nonzero approximation errors can
be established. Boundedness of the coefficients does not itself
establish those errors. Erdős’s 1948 argument is itself a proof for the
specific Lambert series: it chooses arguments by a system of congruences
so that the divisor counts along a block are divisible by increasing
powers of the base, and a tail bound then forces a long run of zero
digits [11].
Boundedness of a signed weight supplies none of that divisibility
input.
The rational identity
A general squared-Lambert identity
The same geometric summation applies to any weight with the stated linear bound.
Proposition 5.16 (The squared-Lambert identity).
For
The identity follows by expanding
At
Proposition 5.17 (The divisor-sum identity).
where
Proposition 5.18 (The gcd-moment identity).
where
Remark 5.19 (Related series). Writing
Diagonal certificates through scale 82
Each row is a finite instance of Definition 1.2, with a link to the
computation producing its witness. The aggregate result covers every
integer scale
Definition of the finite residue test
For windowDiscrepancy),
and
(certifiedKill;
a decidable condition). By completeness (exists_certifiedKill_iff_tail_diff_notMem_int),
for every
| Computation | Exact statement of what was checked | Lean source |
|---|---|---|
| Fixed-window example, depth 16 | ||
| Fixed-window example, depth 9, wider net |
|
|
| Diagonal certificates, 12 base scales |
|
|
| Diagonal certificates, further scales
through |
The same predicate |
One Lean file per scale; endpoint |
| Contiguous lcm-diagonal band through |
For every natural |
|
| Farey denominator bound | Every |
|
| Coprimality-probability / Möbius-square Farey bound | Every |
|
Remark 5.20 (Scope of the table). No row above is cofinal in
its indexing parameter (
Detailed statements
The following statements give the exact hypotheses of the preceding
arguments. We begin with unconditional identities, rank bounds and
finite computations, then pass to the residue and approximation
conditions. A Lean declaration proving a conditional implication retains
that condition as a hypothesis; it does not supply the missing estimate
for
Unconditional structure and finite examples
The rank formulas hold at every stated level. The residue tests and Farey interval below instead give conclusions on specified finite sets of shifts, scales or denominators. This distinction matters when applying the later conditions, which require witnesses at unbounded indices.
Theorem 6.1 (Rationality gives an eventual tail
period). If
Euler’s theorem gives
Theorem 6.2 (Rationality forces unbounded carry
rank). If
and, for every
The recurrence follows from the scaled tails after clearing a
hypothetical denominator of
Theorem 6.3 (Independence of the retained dyadic
sections). For every integer
is linearly independent over
The proof separates one section at a time: the Chinese remainder theorem forces suitable prime divisors in the other affine arguments, while Dirichlet’s theorem makes the selected argument prime. This proves independence, not just the displayed cardinality. In particular, the span of all dyadic sections is infinite-dimensional; that conclusion alone says nothing about rationality of their weighted sum.
Proposition 6.4 (Denominator divisibility forces tail
integrality). If
The denominator results use the following polynomial, defined for
For example,
Here
Proposition 6.5 (A cyclotomic factor remains after
cancellation). If
Here
Proposition 6.6 (Primes in the upper half remain
after cancellation). For
remains after
cancellation. More generally, the source gives the same
product-divisibility conclusion for a multiplier coprime to that
product; it also supplies a sufficient condition on the multiplier’s
prime factors. For the multiplier
The restriction
Proposition 6.7 (A lower bound for the reduced
denominator). For every integer
Bertrand’s postulate
supplies a prime in
Proposition 6.8 (The exact reduced denominator).
At every integer scale
The product is
Proposition 6.9 (Nonvanishing of a signed dyadic
sum). Let
Indeed, every
summand other than
Proposition 6.10 (Small certificates). For each
integer
Consequently, if
Proposition 6.11 (A common certificate for sixteen
shifts). For each integer
Proposition 6.12 (Historical diagonal examples and the
complete band through 82). Let
The checked certificate
table proves
the corresponding depths begin
The historical 28 examples are now a strict subset of the
aggregate theorem
Definitions and elementary identities
The prefix-tail identity and the truncation formula give both directions of the finite residue test. We then specialise the test to LCM shifts and express it in terms of rational approximation. Möbius inversion provides the alternative coefficient weights used in the subsequent estimates.
Initial implications
Definition 6.13 (The scaled tail). For
The series converges because totientTail
Definition 6.14 (The truncated tail difference). For
The sum
is empty when windowDiscrepancy
Definition 6.15 (The central-residue inequality). For
It puts the residue outside both endpoint intervals of width certifiedKill
Proposition 6.16 (The prefix-tail identity). For
every
Thus
Lemma 6.17 (The necessary depth inequality). For
Indeed, its lower
residue bound must be smaller than its upper bound. Thus
Proposition 6.18 (A certificate implies
nonintegrality). For all
The scaled truncation error
satisfies
Theorem 6.19 (Nonintegrality gives a certificate at
some depth). For every
For
the converse to Proposition 6.18, fix a positive
distance from the nonintegral tail difference to the nearest integer.
The normalised error
Definition 6.20 (The least common multiple of the
first integers). Put periodLcm
le_periodLcm
Proposition 6.21 (The Farey gap lemma). Let
then
In
particular, a rational
Proposition 6.22 (An irrationality criterion from
rational approximations). Let
Proposition 6.23 (An irrationality criterion from near
integers). Let
Then
For a binary example, form a number by concatenating the blocks
Proposition 6.24 (A nonsingular evaluation matrix
gives independence). Let
then the family
Proposition 6.25 (The gap between distinct rational
numbers). If
The numerator
Proposition 6.26 (The Möbius identity for
For the first
rearrangement use
Corollary 6.27 (An equivalent irrationality question).
Subtracting the rational number
This is
the same irrationality question in a different series representation.
The notation
Proposition 6.28 (The squared-Lambert identity).
Let
Expand
Definition 6.29 (The squared-Lambert series with
weight
The equality follows from Proposition 6.26 and
Proposition 6.28
with tsum_totient_half_pow_eq_half_add_moebius_sq
Proposition 6.30 (Weight one and divisor sums).
Proposition 6.31 (Totient weight and gcd moments).
where
Observation 6.32 (Comparison of weighted series). For
where
The first equality is Definition 6.29; the second and third are Propositions 6.30 and 6.31. The middle value is irrational by the cited linear independence theorem. The other two rationality questions are not settled in this record. These examples show that the choice of weight matters: an identity with the same denominators does not transfer an irrationality theorem from one weight to another. They do not classify all weighted Lambert series.
Proposition 6.33 (The weight of pairs divisible by a
fixed integer). Let
This follows by multiplying the two
geometric sums
Proposition 6.34 (The sum over coprime directions). The sum over positive coprime pairs satisfies
To see the
normalisation, write every pair of positive integers uniquely as
Proposition 6.35 (A Stern–Brocot recursion with
stopping). For positive integers
Then
Multiplication by the common denominator proves the identity. At the
root
The first term is a mass retained at the current node, not passed
to either child. Thus the probabilistic interpretation is a branching
process with stopping: after division by
They sum to one. The stopping
probability is at least
Proposition 6.36 (Convergence with an explicit error).
In the splitting identity of Proposition 6.35, the sum of the
two child terms is at most
In
particular,
Proposition 6.37 (A numerator polynomial and its
coefficients). For squarefree
For
Proposition 6.38 (Evaluation at two). For
squarefree
Each quotient is
an integer because
Proposition 6.39 (Decomposition by the radical).
For
The first equality
follows from the definition of
The constant in Proposition 6.40 is the value of
Proposition 6.40 (A cyclotomic congruence). Let
where
Proof. To prove the congruence, let
Write
Squarefreeness cannot simply be dropped from this constant formula.
For
Proposition 6.41 (Adjoining a prime: new divisors).
Let
Proof. Splitting the divisors of
At a primitive
Proposition 6.42 (Adjoining a prime: existing
divisors). Let
Proof. Apply Proposition 6.40 to both
Proposition 6.43 (Lambert-series identities). For
an arithmetic function
In particular, if
Weight |
Value |
Status |
|---|---|---|
| |
rational, trivial | |
| |
rational | |
| |
transcendental, since |
|
| |
irrational (Erdős [11]), also proved in Lean (irrational_erdosBorwein_series) |
|
| |
OPEN; this is #249 |
Remark 6.44 (How the identities differ). The coefficients
matter: a result for the constant weight
The equality between the two indexing conventions for tsum_totient_div_pow_two_eq_pnat_half_pow).
The table keeps apart a cited theorem, an ordinary identity and a formal
declaration.
Proposition 6.45 (An affine combination annihilates
the specified divisor terms). Let
This is affine in
For the four multipliers
The zeroth and first moments are zero, while the second is
For a finite truncation of depth
The
difference between
and both parenthesised terms lie between
is sufficient for this four-tail combination to be nonintegral. The bound is derived from these tail enclosures; no optimality for the actual totient tails is asserted. Obtaining such certificates at the required unbounded family of LCM heights remains unproved, as in Theorems 6.60 and 6.52.
Proposition 6.46 (The error under composite
dilation). For
Indeed,
partition the divisors of
This is an unweighted counting identity. The associated Lambert series satisfies
For the totient series the
required divisor-convolution weight is instead
Iterated prime dilations of divisor counts.
Multiplying an argument by a new prime adds exactly one new family of
divisors. For the divisor count
For one prime, the divisors of
Let Erdos249257.SupportDilationDifferences.iteratedDilationDifference_eq_zero_of_cardFactors_le
The source also proves vanishing of the right-hand divisor count for a
list with repeated primes. That is a statement about the condition
For example, with
Thus the bound
Equivalent quantified certificate conditions
Completeness identifies the base residue condition and the LCM-diagonal condition with irrationality. The following statements spell out the quantifiers and the implications between them. The existence of the required certificates beyond every threshold remains unproved.
Theorem 6.47 (The quantified certificate condition is
equivalent to irrationality).
Theorem 6.48 (It suffices to use multiples of a
period).
Theorem 6.49 (The diagonal condition is equivalent to
irrationality).
Lemma 6.50 (Nondivisors in a short LCM window).
Let
Proposition 6.51 (Totient factorisation on an LCM
progression). Let
The two
factors in
Theorem 6.52 (Rationality forces tail integrality on
an LCM grid). If
Thus all tails at positive multiples of
Theorem 6.53 (A sufficient nonintegrality condition
on the grid). Suppose that for every
Then
The diagonal choice is
Corollary 6.54 (Equivalent conditions stated without
certificates). The series
Equivalently,
for arbitrarily large
Proposition 6.55 (Soundness of a second-difference
certificate). Let
then
For
The finite-grid test compares these
integer numerators modulo
Theorem 6.56 (A finite-grid condition gives a
nonintegral pair). Let
Then
Proof. The tail identity and its elementary bound give
Suppose all pairwise tail differences are integers. Choose
For example, take
| 1 | 2920 | 854 | 3 | 3484 |
| 2 | 2024 | 1694 | 1 | 3200 |
| 3 | 3532 | 2534 | 4 | 3832 |
| 4 | 3796 | 3374 | 1 | 876 |
The last column exceeds
The size hypothesis is
Theorem 6.57 (A sufficient quantified finite-grid
condition). Suppose that for every
Proposition 6.58 (A finite carry test implies
nonintegrality). For each integer
Suppose that for every such
Then
Theorem 6.59 (The block norm condition implies
irrationality). Suppose that for every integer
and
Then
Theorem 6.60 (A four-tail residue criterion).
For nonnegative integers
Then
Consequently the finite condition
implies
The error bound groups the remainder as
Each parenthesis is nonnegative and at most
Consequences
The next conditions concern a single LCM-diagonal tail difference.
For
For
If
Two finite quantities will also recur. With
The
prescribed odd depth used below is
Thus
The numerator is
even, since the totient arguments exceed
Proposition 6.61 (An equivalent diagonal nonintegrality condition). The following statements are equivalent:
This is an exact reformulation of irrationality, not a weaker theorem about a finite set of scales. The later sufficient conditions seek a finite inequality that establishes the right-hand side.
Proposition 6.62 (A sufficient short-window
condition). Suppose that for every
It places the residue away from both
endpoints of the modulus interval. The examples at
Proposition 6.63 (A sufficient approximation
condition). Use the prescribed index
Then
Proposition 6.64 (A sufficient upper-endpoint
separation). Let
Define the finite condition
Then
The sign theorem forces an integral tail to give a residue in the upper endpoint interval. This one-sided test excludes that interval; it does not require a lower residue bound. Both the sign-range hypothesis and the strict modulus bound are essential premises of this implication. The required unbounded family is not established.
Proposition 6.65 (Relations among the sufficient conditions). The sufficient conditions do not form a single linear chain. The proved implications are
There is also a separate sufficient argument:
terminal dominance and flexible centred magnitude each imply the
two-sided exclusion in Proposition 6.66, which implies diagonal
nonintegrality. These statements refer to the quantified versions, with
the bounds on
Proposition 6.66 (An exact endpoint formula).
Let
If
Consequently either of the inequalities
is sufficient for
Proposition 6.67 (A sufficient extension of the examples through exponent 6). The supplied finite result is
The witnesses at
Proposition 6.68 (A sufficient extremal-order
condition). Let
then
If instead the middle value is strictly larger than both outer values, the displayed second difference is negative. In each case the claim follows by adding the two strict differences. No lower bound on their sizes is needed.
For
Proposition 6.69 (A directed certificate condition).
For fixed
exists if and only if
Proof. The exact truncation identity leaves an error
At
Proposition 6.70 (A sufficient condition at the
prescribed mod-four pulses). Suppose that for every positive
integer
and every integer
Then
The mod-four congruence is supplied by Proposition 6.91; exclusion at the
same prime is not. Restricting to
Proposition 6.71 (The full quantified condition).
This is exactly the quantifier structure
Proposition 6.72 (One diagonal parameter suffices). The following condition is equivalent to irrationality:
For a
hypothetical rational value, let
Proposition 6.73 (A sufficient condition on the LCM grid).
One residue certificate
anywhere on the two-multiplier LCM cone, at arbitrarily large
Proposition 6.74 (A finite-grid certificate
condition). Let
then
Proposition 6.75 (Unbounded Farey bounds imply
irrationality). The Farey-gap denominator bound at window
(that is, the proved exclusion bounds are arbitrarily large), then #249 follows via the denominator-exclusion implication, without assuming the certificate supply in Proposition 6.71. No unboundedness claim is proved or attempted in the record.
Proposition 6.76 (The lower bound and a false
proposed upper bound). By Prop. 6.98, the canonical dyadic
totient-kernel family is unconditionally
Proposition 6.77 (Soundness of the finite carry
test). For fixed
then
Further exact identities
We now bound the errors in expansions of tail differences, without assuming residue separation. Such bounds determine whether a proposed rational centre stays far enough from the integers after the omitted terms are restored.
Proposition 6.78 (The exact totient difference on an
LCM progression). Put
Then
Here
Proposition 6.79 (A lower bound for the totient of a
rough integer). Let
If
Proposition 6.80 (Positivity of the short-window
differences). For
The proof treats divisor offsets and the exceptional prime-power offsets separately, using multiplicativity and the rough-integer estimate of Proposition 6.79. No rationality hypothesis is used. Positivity of these finitely many coefficients contributes to the later sign theorem; a bound for the remaining infinite tail is still needed to obtain that theorem.
Proposition 6.81 (The accumulated sum is the
discrepancy). For all
Thus its two-sided residue inequality is precisely
Proposition 6.82 (A global-to-local identity).
Thus a separation
estimate for
Proposition 6.83 (A rational approximation with an
error bound). For all
The triangle inequality
transfers a separation estimate between the real tail and its rational
approximation at the cost of this error. The bound tends to zero with
Proposition 6.84 (Unconditional positivity). For
with no irrationality hypothesis; the true,
infinite, real translated tail difference is strictly positive
throughout almost the entire short window, proved unconditionally from
Prop. 6.80 plus a
directed one-sided tail bound. Any argument about the sign of the actual
orbit (not merely its residue mod
Proposition 6.85 (The residue forced by integrality).
Let
If
The later tail difference is a positive integer.
Its negative is the representative near zero, while the least
nonnegative residue lies near
Proposition 6.86 (The penultimate term of a partial
divisibility pattern). Let
Then
Indeed,
Proposition 6.87 (An equivalent test using two
residue bits). For every
The last interval says that the two leading bits
are
Proposition 6.88 (The factor in a second difference).
Let
To see the
factor, set
Also
Proposition 6.89 (Carry displacement and tail
integrality). For a positive integer
The recurrence and the limit identify
Proposition 6.90 (A consequence of rationality and
its limitation). If
Proposition 6.91 (A totient difference congruent to
two modulo four). For every positive integer
To construct
Proposition 6.92 (A prescribed residue after a long
divisibility block). Let
The construction uses
Thus the first
If
The initial integer is
multiplied by
Proposition 6.93 (A Möbius-inversion formula for the tail).
For
Indeed,
substitute
Proposition 6.94 (Explicit finite examples). The
finite certificates
Proposition 6.95 (The necessary depth). Every
certificate
The
two endpoint margins must fit inside an interval of length
Proposition 6.96 (Rationality gives an eventual tail
period). Suppose
The identity relating
Proposition 6.97 (Tail integrality on an LCM grid).
If
The threshold may depend on the hypothetical rational value. A certificate at one fixed scale therefore gives a finite denominator exclusion, not irrationality. Proposition 6.73 requires certificates at arbitrarily large scales, so that one lies beyond the threshold supplied by any such rational value.
Proposition 6.98 (Independence of the retained dyadic
family). For every
Proposition 6.99 (The exact range of the stated
Farey-gap inequality). Let
one has
The first failure occurs at
obtained from the stated Farey mediant. Thus the range is exact for this
particular inequality. It is not an optimality claim among all
denominator-exclusion tests. The preceding range gives the exclusion in
Proposition 6.100,
approximately
Proposition 6.100 (The resulting denominator
exclusion). For every reduced fraction
This is an unconditional finite denominator exclusion. It does not assume certificates at arbitrarily large scales, as required by Proposition 6.71. Conversely, excluding this finite range does not rule out rational values with larger reduced denominators.
Proposition 6.101 (Two general irrationality
criteria). Let
Another is
that, for every integer
Indeed,
if
Proposition 6.102 (Lambert identities involving
Proposition 6.103 (A general rational gap bound).
If
since
These
lower bounds tend to infinity precisely when
Proposition 6.104 (Diagonal certificates through
where
Proposition 6.105 (A coprime-pair expression for
For independent random variables
Counterexamples and limitations
A residue or coefficient condition may hold for a rational comparison
series as well as for
Observation 6.106 (The sign of the actual endpoint
representative). Assume
The tail recurrence gives
Thus the representative
corresponding to the actual tail is negative. The stated size bound
allows it to remain in the endpoint interval, so its sign alone does not
contradict integrality. Other integers in that interval with the same
residue need not represent the actual tail. Proposition 6.85 gives the further
residue separation that would exclude this case. actualLcm_trueEndpointSurvivor_neg
Observation 6.107 (The complete divisibility pattern is
impossible). Let
The simultaneous divisibilities
cannot hold. The terminal difference would be positive
by Proposition 6.80, smaller than not_actualLcmTerminalDyadicStaircase_of_room
Observation 6.108 (An exact valuation in a dyadically scaled
family). For every integer
Indeed, the three arguments are fixedRankSecondDifference_dyadic_fixture_exact
Observation 6.109 (A rational sequence with matching parity).
Start with the coefficient sequence
The
resulting sequence has the same sum parityCoboundaryWeight
Observation 6.110 (What the parity example disproves). The
sequence
and is not eventually periodic.
More precisely, for every exists_totientParity_arbitrarilyManySeparatedCarry_rational_countermodel
Observation 6.111 (A Mersenne factor does not force
tail-difference divisibility). For the completely multiplicative
sequence
If idCoeff_mersenneModulus_does_not_annihilate_tailShift
Observation 6.112 (A lower bound for the stated reconstruction
cost). Let
Indeed, three_le_totientAdjugateTailCost
Observation 6.113 (A second-difference test need not use less
depth). For
The second-difference certificate is the finite inequality
It
implies totient_tail_rank_two_kill_sound_but_not_shallower_cell
Observation 6.114 (The prime-power restriction in the unit-gap
refinement). The ordinary interval test excludes a rational denominator
when its possible numerator interval contains no integer. Reduced
fractions permit a refinement: every numerator is coprime to its
denominator, so an interval containing only nonunits can also be
excluded. For a candidate
After subtracting an integer multiple of
Thus a successful refined certificate at a
prime-power denominator has at most one candidate integer. This is not a
bound for an arbitrary window:
Both candidates reducedDenominatorCandidateCount_prime_pow_le_one).
Observation 6.115 (A synthetic sequence preserving the stated
LCM differences). Here is the recurrence behind the comparison. Fix
The index
The equality follows because all prime divisors of
The triangle inequality gives the precise uniform bounds
These are uniform in
Finite shift polynomials therefore preserve the recurrence, but not
the original numerical bounds independently of their coefficients. This
comparison does not identify lcm_factorIdeal_finiteRank_shiftAlgebra_not_sufficient.
The decomposition of the actual totient into divisor contributions is
proved in Lean (totient_eq_sum_mobiusTotientChannel).
Observation 6.116 (Compatible carries for fixed-precision
local symbols). For example, prescribing an odd coefficient modulo
At each step, reduce
Solving for
fixedPrecisionTropicalNoGo
Observation 6.117 (Correction-free factorisation does not ensure nonvanishing). Consider the two finite differences
They arise from the
square-congruence choice
again with coprime factors at
every term. The square-CRT construction removes the non-coprime
multiplicativity correction on the prescribed finite range. That
property alone does not imply nonvanishing. These are explicit witnesses
of the two possibilities, not a claim that the first is a smallest
counterexample. squareCRT_clean_block_can_vanish
Observation 6.118 (No fixed integer clears every primitive
denominator). Let
These follow by subtracting
consecutive prime-power values of no_fixed_integral_primitive_euler_index
Observation 6.119 (A finite exclusion is not a membership
test). A successful residue certificate proves the exclusion stated in
its soundness theorem. Failure of that sufficient condition at finitely
many depths does not prove integrality of the tail difference. In
particular, a finite unsuccessful search cannot be substituted for the
eventual-period assertion needed to prove rationality. The same logical
distinction occurs for the linked greedy test in a separate Mersenne
achievement-set problem: its finite inequality implies nonmembership.
The linked object is a definition, with a soundness theorem in the same
file, not a theorem asserting a universal impossibility of finite
rationality proofs for Problem #249. Membership or rationality
established by some additional exact identity is not excluded by this
observation. Likewise, the successful finite ranges in
Propositions 6.94
and 6.104 remain
finite ranges until an unbounded supply is proved. CertifiedGreedyMersenneDeath
Parameter ranges and quantifiers
The distinction between a finite calculation and an unbounded family
is in the quantifiers. A statement such as
Some identities have no distinguished scale parameter. They are listed with the general identities. An equivalence can hold for all parameters without establishing either of the equivalent arithmetic assertions.
The LCM formulation of Problem 249 requires arbitrarily large scales:
irrational_totientSeries_iff_actualLcmOrbitNonintegralitySupply
a cofinal statement in the exponent
The table groups statements by their parameter ranges, not by proof status. In particular, some assertions with cofinal quantifiers are already proved, such as the prime constructions and rational comparison sequences. Others are implications whose quantified hypotheses remain open. The horizontal rule separates the cofinal group for ease of reference; it does not mark a boundary between proved and unproved mathematics. The descriptions identify this distinction in that group. The prefixes summarise the quantifiers; complete hypotheses are given in the cited statements. A definition records an object or condition; it does not by itself prove the associated soundness or existence assertion.
In the periodic-weight rows, write
Result |
Source | Quantifier prefix | Representation |
|---|---|---|---|
Result |
Source | Quantifier prefix | Representation |
| scaled totient tail (definition) | totientTail |
|
binary-weighted series |
| integer prefix and real tail | two_pow_mul_totient_series_eq |
|
binary-weighted series |
windowDiscrepancy |
|
finite binary sums | |
certifiedKill |
|
finite binary sums | |
| necessary depth inequality | certifiedKill_depth_floor |
|
finite binary sums |
| residue test soundness | tail_diff_notMem_int_of_certifiedKill |
|
finite binary sums |
| completeness of the residue test | exists_certifiedKill_iff_tail_diff_notMem_int |
|
finite binary sums |
| integrality from denominator divisibility | tail_diff_int_of_den_dvd |
|
binary-weighted series |
| tail-period law | eventual_period_of_not_irrational |
|
binary-weighted series |
| least common multiple |
periodLcm |
|
LCM periods |
| a nondivisor below |
eq_prime_pow_of_not_dvd_periodLcm |
|
LCM offsets |
| totient factorisation at divisor offsets | totient_periodLcm_ray_split |
|
totient factorisation |
| integrality on the LCM grid under rationality | rational_totient_series_forces_lcm_cone_flatness |
|
LCM grids |
| second-difference residue test | second_diff_notMem_int_of_certifiedRank2Kill |
|
finite binary sums |
| a nonintegral pair on a finite grid | exists_nonintegral_pair_of_coneNonflatCert |
finite |
finite LCM grids |
| finite exclusion of integer carries | tail_diff_notMem_int_of_survivorKill |
|
integer recurrences |
| Farey neighbour denominator law | farey_gap |
|
rational intervals |
| rational-approximation criterion | irrational_of_den_mul_abs_sub_tendsto_zero |
|
general criterion |
| near-integer irrationality criterion | irrational_of_int_mul_near_int |
|
general criterion |
| independence from a nonsingular evaluation matrix | linearIndependent_of_separatedMinorCertificate |
a finite family with a square evaluation matrix of nonzero determinant | general criterion |
| dyadic totient-kernel rank |
linearIndependent_canonicalTotientKernelFamily |
|
dyadic sections |
| rationality forces unbounded carry-kernel rank | not_irrational_totientSeries_implies_unbounded_carryRank_unconditional |
|
carry sections |
| no fixed |
no_fixed_integral_primitive_euler_index |
|
Möbius sums |
| Lambert-series value identities | tsum_totient_div_pow_two_eq_pnat_half_pow |
value identities, |
Möbius sums |
| prime-power unit-gap criterion | reducedDenominatorUnitGapCert_prime_pow_iff |
|
rational intervals |
| positive rational-difference lower bound | positive_rational_difference_lower_bound |
|
general criterion |
tsum_totient_half_pow_eq_half_add_moebius_sq |
unconditional | Möbius sums | |
| weighted squared-denominator identity | tsum_lambert_linear_weight_sq_pure |
|
Möbius sums |
| Proposition 5.14 | unconditional | Möbius sums | |
tsum_one_div_mersenne_sq_eq_sigma_sub_tau_series |
unconditional | Möbius sums | |
tsum_totient_div_mersenne_sq_eq_gcd_moment_series |
unconditional | gcd moments | |
| comparison of the weights | Propositions 5.14–5.18 | unconditional | Möbius sums |
| gcd-divisibility factorizes | tsum_pos_pair_both_dvd_half_eq_inv_mersenne_sq |
|
geometric weights |
| sum over positive coprime pairs equals
|
tsum_pos_coprime_inv_mersenne_eq_one |
unconditional (sum over all coprime pairs) | geometric weights |
| Stern–Brocot recursion with stopping | cylinderMass_split |
positive integers |
Stern–Brocot tree |
| positive numerator coefficients | mobiusNumeratorPolynomial_eq_gcdWord |
|
divisor and cyclotomic sums |
| evaluation at |
mobiusNumeratorPolynomial_eval_two |
|
divisor and cyclotomic sums |
| reduction to the radical of |
scaledMobiusShadow_eq_radicalBase |
|
Möbius sums |
| numerator congruence modulo |
cyclotomic_dvd_mobiusNumeratorPolynomial_sub |
|
divisor and cyclotomic sums |
| gcd of the numerator and |
mobiusNumerator_gcd_cyclotomicValue |
|
divisor and cyclotomic sums |
| Mersenne factors retained in the denominator | upperHalfChannel_product_dvd_den_of_scale_primeFactors_le |
|
divisor and cyclotomic sums |
| denominator lower bound / exact value | lcmHeight_scaledMobiusShadow_den_exact |
|
Möbius sums |
| numerator congruence after adjoining a prime | cyclotomic_dvd_primeJump_new_fibre |
|
divisor and cyclotomic sums |
| squared-Mersenne series: partial sum plus tail | mobius_square_series_eq_partial_add_tail |
|
Möbius sums |
| cancellation of the affine divisor terms | joint35_oldChannel_zero |
|
LCM diagonal |
| new-divisor counting identity | supportCoeff_mul_eq_add_defect |
|
divisor counts |
| bound on zero blocks in divisor counts | supportCoeffZeroWindow_length_le_eps_logb_add |
|
divisor counts |
| equivalent shift condition for the target
|
shiftWindowZero_iff_half_mem_mersenneAchievementSet |
iff, no extra parameter | Mersenne subsums |
| totient multiplication with common prime factors | totient_mul_eq_overlapFactor_mul |
|
totient identities |
| totient relative-Euler-product split | totient_mul_eq_totient_mul_relativeEulerProduct |
|
totient identities |
| formula for |
lcmRayArithmeticLetter_eq_deltaTotient |
|
Möbius sums |
| the finite diagonal sum equals |
lcmDiagonalArithmeticWord_eq_windowDiscrepancy |
|
Möbius sums |
| #249 |
irrational_totientSeries_iff_actualLcmOrbitNonintegralitySupply |
iff | Möbius sums |
| the LCM tail difference is an integer
translate of a multiple of |
actualLcmTailOrbit_eq_scaled_totientSeries_sub_prefix |
|
Möbius sums |
| explicit finite-block approximation | abs_actualLcmTailOrbit_sub_rawApprox_lt |
|
Möbius sums |
| an equivalent residue-interval condition | exists_certifiedKill_iff_guardCylinderWitness |
|
integer recurrences |
| sign of the three-term totient difference under the stated middle-value bound | fixedRankSecondDifference |
|
totient differences |
| exact value on a specified dyadic family | fixedRankSecondDifference_dyadic_fixture_exact |
|
totient differences |
| the rational parity comparison (definition) | parityCoboundaryWeight |
|
binary-weighted series |
totientTail_eq_tsum_positiveForeignResidueKernel |
|
divisor and cyclotomic sums | |
totientTail_eq_tsum_shiftedMobiusPulse |
|
divisor and cyclotomic sums | |
| absolute convergence and regrouping of Lambert sums | tsum_lambert_pair_regroup_if |
|
divisor and cyclotomic sums |
| carry divisibility and integral tail differences | carryShift_dvd_iff_tailDiff_mem_int |
|
integer recurrences |
| rationality |
not_irrational_totientSeries_implies_mod_period_and_unbounded_rank |
|
integer recurrences |
| the stated reconstruction cost is at least
|
three_le_totientAdjugateTailCost |
|
weighted tail bounds |
| directed residue interval (definition) | directedCertifiedKill |
|
integer recurrences |
| rationality and an integer carry with vanishing boundary term | binaryCoeffSeries_rational_iff_exists_temperedBinaryOrbit |
|
binary-weighted series |
| doubling-orbit rigidity | doublingOrbit_eq_zero_of_tempered |
|
integer recurrences |
| number of labels needed for exact tail recovery | balancedPulse_no_autonomous_decoder |
|
binary-weighted series |
| endpoint residues do not determine the initial carry | affineBinaryOrbit_mod_twoPow_eq |
|
binary-weighted series |
| integer-coefficient block-certificate dichotomy | int_coeff_series_irrational_or_bpow_mul_eq_intCast_of_full_block_certificates |
|
binary-weighted series |
| divisibility under iterated forward differences | dvd_iteratedForwardDifference |
|
integer sequences |
| totient series as a coprime-pair sum | tsum_coprime_pair_pow_eq_tsum_totient_mul_pow |
|
geometric weights |
| factorisation through a rational-valued linear functional | linearDescender_eq_smul_eval |
rational vector spaces |
divisibility and linear algebra |
| divisibility of a reduced denominator | divisor_dvd_divInt_den |
|
divisibility and linear algebra |
| the complementary denominator divides the integer multiplier | scalarLocalization_complement_dvd |
|
divisibility and linear algebra |
| largest-exponent nonvanishing criterion | scaled_dyadic_sum_ne_zero |
|
divisibility and linear algebra |
| column rescaling and determinant nonvanishing | det_residualMonomialMatrix |
|
complex matrices |
| determinant |
incidenceMobius_det_eq_one |
|
Möbius sums |
| error bound from convergence | controlledForeignProjection_of_tail_limit |
|
Möbius sums |
| carries realising fixed-precision unit residues | fixedPrecisionTropicalNoGo |
|
divisibility and linear algebra |
| vanishing of iterated prime dilation differences | iteratedDilationDifference_eq_zero_of_cardFactors_le |
distinct primes |
divisor counts |
three_quarters_mul_lt_totient_of_rough_lt_two_pow |
|
Möbius sums | |
| positivity of short-window totient differences | lcmRayArithmeticLetter_pos_of_lt_two_mul |
|
Möbius sums |
| the negative representative of the true endpoint | actualLcm_trueEndpointSurvivor_neg |
|
Möbius sums |
| integrality forces upper-endpoint residue | actualLcm_integral_forces_topEdgeResidue |
|
Möbius sums |
| terminal dyadic staircase impossible under the size condition | not_actualLcmTerminalDyadicStaircase_of_room |
|
Möbius sums |
| penultimate difference in a partial divisibility pattern | puncturedDyadicStaircase_penultimate_eq_half |
|
Möbius sums |
| upper-endpoint residue-gap |
actualLcmTailDiff_notMem_int_of_topEdgeResidueGap |
|
Möbius sums |
| relation between the centred residue and the actual carry | two_mul_actualOddHalfCenteredLift_eq_terminal_sub_trueCarry |
|
Möbius sums |
| divisibility of the three-term totient difference | two_mul_totient_dvd_fixedRankSecondDifference |
|
totient differences |
| equality of two finite rational approximations | renormalizedResidueAgreement_of_twice_le |
|
Möbius sums |
| a Mersenne divisor need not divide a tail difference | idCoeff_mersenneModulus_does_not_annihilate_tailShift |
|
Möbius sums |
| finite numerator separation implies nonintegrality | scaleFullTarget_miss_of_lambert_projected_num_gap |
|
Möbius sums |
| periodic-weight Lambert dichotomy | irrational_or_bpow_mul_eq_intCast_intWeightedErdosSeries_periodic |
|
Möbius sums |
| periodic weight with nonnegative divisor coefficients | irrational_intWeightedErdosSeries_periodic_of_coeff_nonneg_of_frequently_ne_zero |
|
Möbius sums |
| zeros on one progression for the character modulo four | intWeightedCoeff_periodFourSignWeight_eq_zero_of_mod_four_eq_three |
|
Möbius sums |
| positivity of the translated LCM tail difference | actualLcmTailDiff_shift_pos |
|
Möbius sums |
| Farey window |
gap_check_window_1_240_le_79639646646701375323355774875831053 |
|
rational intervals |
| denominator lower bound |
tsum_totient_div_pow_two_ne_ratCast_of_den_le_79639646646701375323355774875831053 |
|
rational intervals |
| finite LCM certificates covering
thresholds |
powerTwoActualLcmShortArithmeticKillSupply_through_six |
|
Möbius sums |
| contiguous diagonal certificate band
through |
ErdosProblems.Skip.LadderT67.exists_diagonalKill_le_82 |
|
LCM diagonal |
| residue certificates for |
certifiedKill_all_small |
|
finite binary sums |
| denominator exclusions for |
totient_series_ne_rat_of_den_dvd_pow_two_mul_mersenne_upto_sixteen |
|
finite binary sums |
| the second-difference test uses more depth
at |
totient_tail_rank_two_kill_sound_but_not_shallower_cell |
first-difference certificate at |
finite binary sums |
| listed diagonal certificates with |
certifiedKill_diagonal_all_imported |
|
LCM diagonal |
| LCM certificates at |
lcmDiagonalArithmeticKill_two_pow_four |
|
Möbius sums |
| square-CRT coprime-factor examples: zero / nonzero differences | squareCRT_clean_block_can_vanish |
witness |
totient factorisation |
| certificate criterion (proved implication; unproved premise) | irrational_totient_series_of_certificate_supply |
|
finite binary sums |
| period-multiple criterion (equivalent; unproved condition) | irrational_totient_series_of_multiple_certificate_supply |
|
multiples of periods |
| LCM-diagonal criterion (unproved condition) | irrational_totient_series_of_lcm_diagonal_certificate_supply |
|
LCM diagonal |
| LCM-grid certificate criterion (unproved premise) | irrational_totient_series_of_lcm_cone_window_kill_supply |
|
LCM grids |
| LCM nonintegrality criterion (unproved condition) | irrational_totient_series_of_lcm_diagonal_nonintegrality_supply |
|
real tail differences |
| finite-grid residue criterion (unproved premise) | irrational_totient_series_of_lcm_cone_nonflat_supply |
for every |
finite LCM grids |
| first-harmonic norm criterion (unproved premise) | irrational_totient_series_of_first_harmonic_norm_gap |
|
binary-weighted series |
| four-tail residue criterion (unproved premise) | irrational_totient_series_of_primeJumpSharpKill_supply |
|
binary-weighted series |
| short LCM-window criterion (unproved premise) | PowerTwoActualLcmShortArithmeticKillSupply |
|
Möbius sums |
| LCM-tail separation criterion (unproved premise) | irrational_totientSeries_of_actualLcmOrbitSeparationSupply |
cofinal |
Möbius sums |
| five endpoint criteria (unproved premises) | irrational_totientSeries_of_flexibleActualTerminalDominanceSupply |
one of the five quantified conditions in Proposition 9.14 | Möbius sums |
| proved rational counterexample to bound, parity and aperiodicity | exists_totientParity_arbitrarilyManySeparatedCarry_rational_countermodel |
|
binary-weighted series |
| proved mod-4 prime construction (CRT and Dirichlet) | exists_prime_deltaTotient_four_mul_mod_four_two |
|
Möbius sums |
| sufficient mod-4 condition (unproved premise) | irrational_totientSeries_of_cofinal_modFourPulseSurvivorKill |
the displayed mod-four residue condition at arbitrarily large scales | Möbius sums |
| proved two-adic prime construction | exists_prime_totient_twoAdic_pulse_divisors |
|
divisibility and linear algebra |
| proved implication from eventual integrality | eventual_integral_tailDiff_has_cofinal_twoAdic_half_pulse |
|
divisibility and linear algebra |
Finite extension and cofinal estimates
Extending a computation supplies more finite witnesses. To reach a cofinal statement, an argument must instead produce a witness beyond an arbitrary threshold. The examples below specify which of these extensions is needed; the largest computed scale is not asserted to be a limit of the method.
Finite certificate tables. Results such as the diagonal certificates at 28 explicit values of
through , now a strict subset of the aggregate band (certifiedKill_diagonal_all_imported), the certificates for at fixed depth 16 (certifiedKill_all_small), and the exclusions for at exponent 14 (totient_series_ne_rat_of_den_dvd_pow_two_mul_mersenne_upto_sixteen) are each a finite list of independently verified rows, not a single argument instantiated at a free parameter. The existing lists do not establish further rows; an extension needs either additional computations or an argument for a family of parameters.A bounded window inside a uniform theorem. The rough-integer bound of Proposition 6.79 and the positivity theorem of Proposition 6.84 hold for every
, subject to their stated bounds on the other parameters. In the sign theorem, for example, . Their proofs are therefore not merely enumerations of a fixed set of exponents. The missing conclusion is a suitable residue inequality at arbitrarily large scales, not extension of the range of in the positivity theorem. No complexity lower bound follows from these examples.Parameter dependence in an approximation estimate. For reduced approximants
to , the conditions and imply irrationality. A growing denominator alone does not control this product. In particular, the exact reduced-denominator formula of Proposition 6.8 concerns a specified finite Möbius sum; it does not estimate the complementary tail. Likewise, a bound proved with a constant depending on a fixed auxiliary parameter is not automatically uniform when that parameter grows. Both the dependence of the constant and the error estimate must be retained in any passage to an unbounded family.
The missing arithmetic inputs include the stated constant-saving exponential-sum estimate and an upper-endpoint residue inequality. For the positivity theorem, the unresolved step is exclusion of that residue interval, not positivity at more exponents.
Relations between the representations
Binary tails, Möbius sums, rational approximations and exponential
sums express related information about
- Binary-weighted series and tails.
-
The coefficients in
are unbounded; this expression is not the base-two digit expansion of . The tail , finite difference numerator and test retain this coefficient information. The identity(
tsum_totient_half_pow_eq_half_add_moebius_sq) and its partial-sum version (mobius_square_series_eq_partial_add_tail) express the same value by Möbius sums. An equality of values does not by itself transfer a claim about the original coefficient subsequences. - Lambert sums and finite numerator polynomials.
-
The Lambert identities for
, and give the series relations in Section 5. For a finite divisor sum, the polynomial evaluation (mobiusNumeratorPolynomial_eval_two) and the definition (mobiusNumerator) put its numerator into integer polynomial arithmetic. This evaluates a finite contribution, not the complementary infinite tail. - Coprimality probability.
-
Let
be independent with for . Then . The divisibility probabilities are (tsum_pos_pair_both_dvd_half_eq_inv_mersenne_sq). Möbius inversion converts these to the coprimality probability. The decomposition by the greatest common divisor also gives the weighted coprime-pair identity (tsum_pos_coprime_inv_mersenne_eq_one). Counting coprime pairs by their sum gives the totient expression directly (tsum_coprime_pair_pow_eq_tsum_totient_mul_pow). - Cyclotomic factors of finite denominators.
-
The coefficient formula for
(mobiusNumeratorPolynomial_coeff) and the cyclotomic divisibility statement (cyclotomicValue_dvd_baseMobiusShadow_den) identify factors in the reduced denominators of the specified finite sums. The product-divisibility theorem (upperHalfChannel_product_dvd_den_of_scale_primeFactors_le) is used in the exact denominator formula (lcmHeight_scaledMobiusShadow_den_exact). Growing finite denominators alone do not exclude cancellation with the remaining tail. - Numerator divisibility and denominator bounds.
-
Write
in lowest terms, with . For and a positive divisor of , if the reduced denominator of divides , then (scalarLocalization_complement_dvd). In particular, when . A related bound isfor integers
(positiveRat_mersenne_height). Here positivity gives ; the size inequality then gives the conclusion. These are arithmetic bounds on a reduced fraction, not irrationality criteria without an additional approximation estimate. - Farey intervals.
-
The denominator bound (
farey_gap) applied to the explicit window gives (gap_check_window_1_240_le_79639646646701375323355774875831053) and hence for integers and . The finite input is a totient numerator modulo . Its exact first failing denominator is , the denominator of the relevant Farey mediant (gap_check_window_1_240_first_failure). This last assertion concerns this fixed window. - Differences at least-common-multiple shifts.
-
For
(periodLcm), a jump in can occur only at a prime power (eq_prime_pow_of_not_dvd_periodLcm). The identities (lcmRayArithmeticLetter_eq_deltaTotient) and (diagonalWindowIncrement_eq_lcmRayArithmeticLetter) identify the coefficient difference as and give . Thus these arithmetic formulas concern particular instances of the same finite residue test; additional window restrictions remain in force. - Exponential sums of the window residues.
-
For integers
, the relevant block statistic isA bound by
, together with and , yields a certificate in the block (exists_certifiedKill_of_first_harmonic_gap). The linked irrationality implication uses the stronger complex norm bound , for every on arbitrarily late blocks satisfying the same size inequality (irrational_totient_series_of_first_harmonic_norm_gap). The finite implication uses ; the required cancellation bound is still unproved. The norm bound on the complex exponential sum is sufficient for the displayed real-part bound, but is stronger.
Binary tails and Möbius sums
Erdős’s argument for
A different proposal would recover each later block from a fixed
finite summary of the preceding history. The counterexample of
Proposition 2.11(i) (balancedPulse_no_autonomous_decoder)
shows why that proposal fails for the family constructed there. For
The implication from the quantified certificate condition (irrational_totient_series_of_certificate_supply)
is a separate theorem. The counterexample above neither proves its
hypothesis nor makes it the only possible route to irrationality.
Likewise, Proposition 10.4
shows that inverse-phase column weights can preserve a determinant, and
Theorem 6.3
gives the exact growing ranks of totient sections. These are different
statements with different hypotheses; none is a general prohibition on
other representations of
The Möbius representation instead allows the squared-Lambert identity
of Proposition 5.16 to be applied to
Index of unproved conditions
Every condition in this index is accompanied by the implication that
would turn it into irrationality of
Scope of the index
The index compares particular quantified hypotheses and the results that use them. An unsuccessful implication between two entries therefore says nothing by itself about every argument using the same method.
Each entry states its quantifiers in full. A cofinal assertion, with
a quantifier of the form
The quantified residue condition for #249, stated in Definition 1.2 and proved sufficient (irrational_totient_series_of_certificate_supply),
is the following statement:
The following catalogue compares fourteen proposed approaches to this condition. It starts with the exponential-sum estimate, then gives thirteen further approaches with their individual hypotheses and source references.
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
Proved results and the additional assumptions they need
Besides the exponential-sum condition, the sufficient hypotheses involve tail signs, endpoint residues, rational approximation, short windows, Farey bounds, divisibility, denominator growth and carry rank. For each, we state the missing estimate used by the proposed application. These are specific possibilities rather than a classification of methods for Problem #249.
Positivity and the remaining residue inequality
Definition 9.9. The actual LCM tail orbit
at exponent actualLcmTailOrbit_pos).
Theorem 9.10. For every
Hence
Remark 9.11 (Which endpoint interval must be excluded). Under
the hypotheses of Proposition 6.85, integrality would
force the residue to be
The one-sided test below excludes precisely that upper interval. This
uses the bound
An exact endpoint identity
Under the bounds below, positivity places an integral tail difference at the upper residue endpoint. A one-sided inequality would exclude it. That additional inequality is a sufficient condition, and is not claimed to be strictly weaker than irrationality.
Theorem 9.12 (The proved implications). For
every
Definition 9.13 (The unproved quantified condition). The upper-endpoint condition is
No unconditional statement anywhere in
the record locates the residue of the diagonal word actualLcmTopEdgeResidueGap_iff_terminal).
PowerTwoActualLcmTopEdgeResidueGapSupply
Proposition 9.14 (Five sufficient conditions).
Each of the five conditions below suffices for irrationality; none of
them is proved. The first four imply the upper-endpoint condition; the
fifth gives nonintegrality directly by the endpoint identity. These are
not asserted to form a linear hierarchy. Here
Adjacent-suffix band:
(a two-sided band on the adjacent-suffix residue directly, one candidate depth
).Odd-prefix interval at the prescribed depth: at the prescribed odd depth
, a two-sided band of half-width on the half-word residue modulo . The depth is fixed by ; it cannot be chosen independently of .Centred-residue bound at the prescribed depth, proved equivalent to the previous one:
Centred-residue bound at a variable depth: the same magnitude bound with the depth restriction relaxed from the prescribed value
to any odd satisfying the half-cell fit and the positivity range .Terminal dominance: under the same bounds as item 4,
. This is a different one-sided comparison, treated immediately below.
For the first four conditions, the relevant implications into the
upper-endpoint condition are as follows: adjacent-suffix band
A bound on the last totient difference
We compare the last totient difference with a centred residue. To use
the comparison for irrationality, it would have to hold for arbitrarily
large
Definition 9.15. The terminal dominance
condition, which is unproved, is the following. Writing
Theorem 9.16 (The proved implication). The
dominance hypothesis at a single odd rank already excludes integrality
of
Observation 9.17 (How the sign and size bounds enter the
contradiction). Use the hypotheses and notation of Proposition 6.66. Under the assumption
Terminal dominance
These bounds do not eliminate either approach: they hold under the
integrality assumption that the approach is intended to refute. They
neither prove nor disprove an unconditional estimate for two_mul_actualOddHalfCenteredLift_eq_terminal_sub_trueCarry,
actualLcm_trueEndpointSurvivor_neg,
actualLcmTailOrbit_notMem_int_of_actualTerminalCarryCorridorEscape).
Proposition 9.18 (A sufficient extension).
Either of the following suffices: (i) the lower-escape branch cofinally,
as displayed just above; or (ii) the two-sided magnitude form (item 4 of
Proposition 9.14),
which asks only
Separation of a rational approximation
Theorem 9.19. Unconditionally, for every
where
Remark 9.20 (Scope of the implication). A cofinal
Definition 9.21 (The additional hypothesis). The cofinal approximation-separation condition, which is unproved, is
This hypothesis is about the real quantity
The short-window examples through exponent 6
Theorem 9.22.
The single witness
Definition 9.23 (The additional hypothesis). The cofinal short-window condition, which is unproved, is
The depth restriction gives a
useful description of the offsets: if
The condition restricts the depth in the ordinary diagonal
certificate criterion. It is not established by pointwise completeness,
which permits arbitrarily large depths. Nor does a successful
short-window certificate by itself yield the fixed
The diagonal certificate table
Theorem 9.24.
at depths
Remark 9.25 (The observed depths are finite data). The
necessary depth inequality of Lemma 6.17 forces
Proposition 9.26 (A sufficient extension).
This asks for a certificate within a fixed additive constant of the necessary logarithmic depth bound. The uniform constant is an additional requirement, not a consequence of the finite data.
One common certificate for sixteen shifts
Theorem 9.27.
The basepoint
Remark 9.28 (Finite simultaneity and the unbounded
condition). The displayed computation concerns only
Proposition 9.29 (Simultaneous certificates with
unrestricted depth). The existence of a function
is
equivalent to irrationality of
Proof. The displayed condition supplies Proposition 6.71’s quantified certificate
condition: for fixed
Conversely, suppose
is nonintegral. Fix
The finite
minimum is positive, whereas the left side tends to zero. For each
This proof gives no quantitative lower bound for the finite minimum as the basepoint or number of shifts grows. It selects a common depth after those parameters are fixed; it does not impose depth equal to the period.
The fixed Farey bound
Theorem 9.30. If
Remark 9.31 (What a larger Farey bound requires). Unbounded
valid denominator exclusions would imply gap_check_window_1_240_first_failure)
proves that the residue inequality fails at the mediant denominator
The existing proofs for individual windows use explicit totient
residues and rational endpoint calculations. Extending that
implementation calls for new finite data; a uniform proof of a growing
bound need not use hard-coded convergents. If
Observation 9.32 (The limited gain from a unit-gap
refinement). The finite unit-gap condition of Observation 6.114 (ReducedDenominatorUnitGapCert)
and its quantified version (PrimitiveReducedDenominatorUnitGapSupply)
are definitions; the latter is not asserted to hold. Two separate
results (reducedDenominatorUnitGapCert_prime_pow_iff,
reducedDenominatorCandidateCount_prime_pow_le_one)
show that, for
Proposition 9.33 (A sufficient extension).
Suppose
A two-adic congruence that does not give a certificate
Theorem 9.34. The theorem is unconditional and
holds for every
Under eventual integrality this transfers
to an integer
Remark 9.35 (Why the central residue still fails the test).
This places the residue at the centre of the residue interval:
Proposition 9.36 (A sufficient accumulated-residue
condition). Suppose that for every integer
Then
The residue margin at an LCM jump
Theorem 9.37 (Arbitrarily large prime-power LCM
jumps). For every
Definition 9.38 (The remaining residue margin). For
Thus canonicalAdjacentSuffixCentralSlack
canonicalAdjacentSuffixDepth
diagonalAdjacentSuffixResidue
The first unproved condition asks for every CanonicalAdjacentSuffixPostJumpSlackSupply,
CanonicalAdjacentSuffixPowerTwoPostJumpSlackSupply).
Each condition implies irrational_totientSeries_of_canonicalAdjacentSuffixPostJumpSlackSupply,
irrational_totientSeries_of_canonicalAdjacentSuffixPowerTwoPostJumpSlackSupply).
The implications are proved; both conditions are unproved.
Remark 9.39 (Finite numerical evidence). All periodLcm_succ_eq_prime_mul_of_strict_jump).
Thus canonicalAdjacentSuffixCentralSlack_eq_of_periodLcm_eq).
Thus the value changes only when the LCM height changes. This reduces
the number of distinct values to study; it does not determine their
signs.
Proposition 9.40 (A sufficient inequality). If,
for every
A certificate for a four-tail combination
Theorem 9.41. Use
The bound
Theorem 9.42 (One explicit witness). For
Thus
Remark 9.43 (Scope of the witness). The quantified hypothesis
asks, for every
At a strict LCM jump,
Denominators of Möbius sums
Theorem 9.44. For every integer
Moreover, some
Indeed,
Bertrand’s postulate makes
Remark 9.45 (Growth of these denominators does not give
approximation of
To apply the diagonal criterion in Theorem 6.49, one must establish this tail nonintegrality at arbitrarily large LCM scales. Denominator growth alone does not supply that condition.
Proposition 9.46 (The additional approximation
hypothesis). A sequence of rationals
This is
the rational-separation criterion of Proposition 6.22: if
A different argument could deduce a residue certificate from the surviving divisor and further information about the complementary term. The denominator theorem alone contains no such separation statement. Neither sufficient argument is established by its lower bound, and these are not claimed to exhaust possible approaches.
Rationality and carry rank
The totient sections have a dimension lower bound, as do the sections of an integral carry under the rationality hypothesis. An incompatible upper bound would finish a rank argument. The rational comparison sequences show why rationality by itself gives no such bound.
Theorem 9.47. For every
Theorem 9.48. If
The proof is given in Section 10.8.
Remark 9.49 (The generic upper-bound inference is false). The
bound false_of_compressedAdjointCertificate).
This excludes those simultaneous requirements, not every argument using
a matrix or its adjugate. Separately, the span of all dyadic totient
sections is infinite-dimensional (Proposition 1.6).
Proposition 9.50 (An additional hypothesis for a
totient-specific rank argument). A rank bound that contradicts the
lower bound
Relations between the sufficient conditions
A fixed saving for the real part or norm of the block exponential sum would give a certificate. The endpoint conditions seek a residue or size bound along an LCM sequence instead. Proposition 9.14 relates the sufficient formulations; the arithmetic estimates required by them remain open.
The generic bounded-rank argument fails for a separate reason: the rational comparison sequence has unbounded section rank. A totient-specific upper bound would require hypotheses not shared by that sequence.
These are statements about the displayed conditions and comparisons, not an exhaustive classification of possible proofs. Some conditions are equivalent to irrationality; others are only sufficient. No relative difficulty, truth probability, or independent formal verification follows from their position in the table.
Counterexamples to proposed deductions
The next constructions produce rational series from coefficients
satisfying selected totient data. Others test a proposed estimate
without changing the coefficients. We specify the retained assumptions
in each case, so that the failed deduction can be distinguished from an
argument using additional properties of
Changing the coefficients after a finite prefix
Proposed argument. The quantified residue condition
requires certificates beyond every starting index. A finite computation
can check many instances, but one fixed inspection bound cannot
establish these quantifiers. The following comparison explains this
limitation without making any claim about all possible irrationality
arguments. Erdos249257.TotientTailPeriodKiller.irrational_totient_series_iff_certificate_supply
Counterexample. Theorem 2.4 gives an explicit splice
construction; its series value, exact reduced denominator and failure of
the separation condition are checked in Lean. Choose an integer
Scope. For each fixed bound
Consequence. The finite-prefix example and the
parity example below are distinct constructions. The former preserves a
prescribed finite prefix; the latter preserves parity and has separated
nonperiodic blocks. Each shows why its own list of assumptions is
insufficient. The recorded finite diagonal examples remain useful
individual certificates, but their number alone gives no assertion at
arbitrarily large scales. Erdos249257.TotientTailPeriodKiller.certifiedKill_diagonal_all_imported_through_t64
A rational series with matching totient parity
Matching totient parity and the bound
Construction. Start with the sequence
Each replacement leaves the binary sum unchanged
because
Proposition 10.1 (A rational series preserving
totient parity and the stated separation properties). There exists
Scope. The displayed bounds, parity agreement and
aperiodicity, including the stated number and separation of the edits,
are jointly compatible with a rational binary sum. They therefore do not
imply irrationality. The sequence
Consequence. The paired edits have zero total
contribution, since
Square-CRT factorisations
For a prime
separates the coprime and divisible cases.
Prescribing a cofactor modulo
The examples in Observation 6.117 show both
possibilities. At squareCRT_clean_block_can_vanish).
All four prime–cofactor products are coprime (squareCRT_vanishing_countermodel_is_clean).
At squareCRT_clean_block_can_be_nonzero),
again with coprime factors (squareCRT_nonzero_countermodel_is_clean).
These finite equalities are checked by exact arithmetic. No minimality
claim about either witness is needed. The general existence theorem exists_squareCRT_clean_horizon
supplies a common base for the stated finite congruence requirements,
not a nonvanishing assertion.
The vanishing example disproves the implication from correction-free
factorisation to nonvanishing; the other example shows that this
factorisation does not force vanishing either. This does not establish
formal independence of two propositions, or exclude an argument using
additional hypotheses. The prime-dilation identity totient_mul_prime_cocycle
and the CRT constructions exists_squareCRT_base,
exists_large_squareCRT_base
remain available with their own prime and residue hypotheses.
A separate elementary identity in the same file concerns alternating
sums. Let
This identity is proved in Lean
(alternating_powerset_sum_eq_zero_of_insert_invariant).
It has no totient hypothesis, but an application must still verify
invariance under the indicated insertion. Neither it nor the congruence
construction supplies the missing nonzero totient difference at a
prescribed LCM height.
The cost of clearing a rational denominator
Clearing a denominator changes the multiplier as well as the
fraction. The example
Lemma 10.2 (Complement divisibility after
multiplication). Write
Indeed, the hypothesis makes Erdos249257.AdelicHeightObstruction.scalarLocalization_integer_eq_mul_num).
If
A related elementary inequality compares a positive numerator with
its denominator. If
Lean
proves this Mersenne instance (Erdos249257.AdelicHeightObstruction.positiveRat_mersenne_height)
and the version with a general positive denominator parameter (positiveRat_numDivisor_mul_lt_two_mul_den).
Positivity of
The accompanying linear-algebra statement has a one-dimensional
quotient. Let
This is factorisation
through the scalar quotient Erdos249257.AdelicHeightObstruction.linearDescender_eq_smul_eval).
A surjection onto a higher-dimensional space would imply only a linear
factorisation through that space, not multiplication by one fixed
vector.
The denominator calculations use two lemmas proved in Lean (Erdos249257.RationalDenominatorSurvival.divisor_dvd_divInt_den,
survivingDivisor_dvd_scaled_divInt_den).
For integers
For a nonzero multiplier, a lower bound for upperHalfMersenneProduct_lower_bound)
can be used when that product is shown to divide
The finite Farey exclusion for
(tsum_totient_div_pow_two_ne_ratCast_of_den_le_79639646646701375323355774875831053).
That numerical exclusion requires the interval and Farey calculation; it
is not a consequence of the scalar lemma alone.
Signed moments and parity
A signed determinant can serve in rational approximation only with both a nonzero numerator and a small error. Here parity proves the first requirement for the particular finite signed sum.
Lemma 10.3 (Nonvanishing from a unique largest
denominator exponent). Let
In particular, the sum is nonzero.
Every term except
Lean also proves a separate determinant expansion from the Leibniz
formula (det_mul_rectangular)
and defines the truncated signed moments truncatedMoment,
hankelDet).
The parity lemma is not derived from that determinant identity. A
determinant application must first identify a sum to which the parity
hypotheses apply.
For the totient series, one would still need suitable configurations at arbitrarily large scales and a denominator-weighted error tending to zero. Nonvanishing alone provides neither. No such family is supplied by these two algebraic statements; compare the separate rank discussion in §10.8. In another base, the analogous argument would require divisibility by a prime factor of that base rather than an unchanged appeal to parity.
Column rescaling and cancellation
A nonzero determinant need not prevent one row from being constant. For example,
The first and
last matrices have determinants
Proposition 10.4 (A nonzero minor survives
inverse-phase column weights). Let
Thus a nonzero determinant remains nonzero while row
The entry formula and the determinant of a product prove the
statement. If row-dependent weights are allowed, the choice rowResidualMonomialMatrix_reconstructs_phasePowerMatrix,
rowReconstruction_zero_row_one).
These are statements about complex matrices, not arithmetic
properties of the totient sequence. In particular, determinant
nonvanishing, even with unit-modulus weights, does not by itself exclude
complete alignment in the indicated row. An application of the
first-harmonic criterion (irrational_totient_series_of_first_harmonic_norm_gap)
needs additional information that excludes such weights or controls the
resulting weighted sum. The example does not require that information to
take the form of an identity coupling different rows, and it does not
rule out determinant arguments that use appropriate additional
hypotheses.
Tail integrality on an LCM grid
The comparison. The diagonal condition (Erdos249257.TotientTailPeriodKiller.irrational_totient_series_iff_lcm_diagonal_certificate_supply)
uses the pair
Eventual equality of fractional parts.
Proposition 10.5 (Tail integrality on an LCM grid).
Rationality makes the fractional parts of
(b
Proposition 10.6 (A finite-grid certificate gives a
nonintegral pair). Let
Then
Scope. Eventual integrality on the LCM grid is a
necessary consequence of rationality, not a claim about the actual
series made without that hypothesis. The finite-grid test uses the
individual one-sided bounds
Neither statement supplies the unbounded family required to decide
#249. Exhibiting a nonintegral tail difference on the LCM grid at
arbitrarily large
The implication from rationality to grid flatness (rational_totient_series_forces_lcm_cone_flatness)
should not be confused with an assertion of flatness for the actual
series. The exact diagonal integrality reformulation and its quantified
converse (diagonal_int_iff_foreignDiagonalDefect_hits_fullTarget,
irrational_totientSeries_of_full_target_avoidance_supply)
give other equivalent forms of the problem. They are not the only such
forms; Proposition 1.8
lists further equivalent certificate conditions.
Consequence. Choosing the least deep tail is the
step that turns a common-fractional-part assumption into an intersection
of arcs. A related finite comparison concerns first and second
differences: at totient_tail_rank_two_kill_sound_but_not_shallower_cell).
This disproves a universal claim of smaller depth for second
differences; it does not show that they can never improve a
certificate.
Exact dyadic rank and the limits of a rank argument
At each level the scalar totient identities supply spanning, while
affine independence excludes any further relations. This computes the
rank, rather than merely proving its unboundedness. The latter already
follows from Coons’s nonregularity theorem in every base
Construction.
Theorem 10.7 (Exact dyadic rank and
infinite-dimensionality). For every
is linearly independent over
The two zero-residue sections need separate treatment because their
arguments
Independence removes the positive-residue coefficients and leaves
not_finiteDimensional_span_fullTotientKernel).
A separate elementary observation concerns a proposed integer identity.
There are no false_of_compressedAdjointCertificate).
The Lean independence theorem is also stated for
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
To describe all integral relations, let
For each omitted index put
For a vector
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
Relation to the series value. Infinite section rank
does not imply irrationality of
The same independence argument also bounds the rank of an integral
carry. If
For every
This is the finite family in the linked statement
(not_irrational_totientSeries_implies_unbounded_carryRank_unconditional);
it contains all carry residues at levels
These
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
A separate finite-dimensional calculation concerns the matrix 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
Further counterexamples and sharp bounds
The table records further counterexamples and sharp bounds. For each proposed deduction it lists the retained hypotheses and the conclusion that fails, together with the source for that argument.
Approach |
Argument and source | Scope and remaining question |
|---|---|---|
Approach |
Argument and source | Scope and remaining question |
Complete terminal divisibility pattern |
Under |
The obstruction is specific to that
pattern and those bounds. If the last divisibility is omitted, the
additional terminal bound of Proposition 6.86 forces the
penultimate difference to be |
| Finite linear combinations of shifted carry recurrences | The explicit sequence in
Observation 6.115 has
|
The constructed coefficients are not
asserted to be actual totient differences. Preserving the displayed
recurrence under shifts therefore does not distinguish them from the
coefficients required in the proposed argument. The full totient divisor
identity |
| Adding three multiplicative scales to an integrality test | For |
Adding these three integrality assertions does not strengthen the first one. A different test involving part of the tail would need an estimate for the part it discards; this equivalence provides no such estimate. The result concerns the displayed four conditions, not every test using several scales. |
| Prescribing valuations and finite unit residues | For the valuations |
The specified residues do not exclude
all finite carry sequences while the higher quotients |
| The information retained by an endpoint residue | For an integer sequence |
The endpoints agree modulo Only reduction modulo |
| Bounded finite-state / autonomous successor decoder for the binary carry | For the family in Proposition 2.11(i), with |
This counterexample concerns states
determined only by the common history of the displayed family. It does
not exclude a state using additional information specific to the totient
sequence. The bound counts labels, not bits; it is not a complexity
theorem about the binary digits of |
| Zeros on a progression versus nonzero coefficients arbitrarily far out | Let |
This rules out nonvanishing on an
arbitrarily prescribed progression, not nonzero coefficients arbitrarily
far out. In fact |
| Using a finite exclusion test to prove membership |
|
The cited test has a sound exclusion implication. The analogous soundness statement for the residue test of this record, Proposition 6.18, also does not make a finite unsuccessful search a proof of integrality. This is a limit of what follows from those tests, not an impossibility theorem for rationality or membership proofs using additional identities. |
| Reconstructing one totient value from a two-tail absolute-value linear combination | For any finite |
The displayed termwise absolute-value
estimate cannot be less than |
| Homogeneous Mersenne-primitive prime factor alone forces a contradiction | For the completely multiplicative
sequence |
A factor of |
| The unit-gap test at a prime-power denominator | For |
This candidate-count bound does not
apply to every odd denominator; the example modulo |
| Extra divisibility of a three-term totient difference | At |
The exact valuation concerns this
scaled family, not the LCM family with |
Signed interpolation with entire Dirichlet defects
The small block
has
coefficient sum
This construction assigns different jobs to the shape and amplitude of a correction. High-order finite differences annihilate low-order moments; their integer amplitudes adjust the series value. As the orders increase, later completed blocks contribute zero to each fixed moment, so its defect stabilises between blocks. The prescribed initial collection of moment defects is zero, not merely constant. Spacing the blocks controls their density and analytic convergence. All corrections occur at even indices, leaving every odd totient fixed. The three numbered remarks below have ordinary proofs; none has yet been formalised in Lean.
For a sequence
Let
Remark 10.8 (Sparse interpolation around the totient). Fix
integers
equals
, , and . In particular the prefix through and every odd coefficient are unchanged.For every fixed
, both and are divisible by eventually, with a cutoff independent of .For every fixed
, the defect equals an integer for all sufficiently large . The cutoff is independent of . If and , this defect is zero at every .For each root of unity
, the radial function extends smoothly to . Its Taylor coefficients there lie in . The coefficients of orders are zero if the order of is at most .For every fixed
the absolutely convergent seriesextends to an entire function, and
.
The set
For large
Thus every block length
Ordinary proof; not formalised in Lean.
The allowance can grow as slowly as desired and need not be monotone.
For
Proof. We construct the blocks first, independently of the target value. Their increasing order enforces the moment and boundary conditions; only their amplitudes will be chosen afterwards to obtain that value. All blocks lie beyond the prescribed prefix.
The tail infimum in
These parameters serve two different constraints.
The inequality
The factor
Bounds for the coefficients. If
At every modified index
because all
odd-prime factors are at least one and the smallest possible factor at
two is
An interval of values. At
The sum
Congruences and moments. For every polynomial
This follows by iterating the forward-difference
operator, which lowers polynomial degree. Eventually
Sparsity and blocks. Within the
The following gaps telescope to
Radial smoothness. The number of differences increases with
the block index, so any fixed derivative order is eventually controlled.
Fix a root
Its coefficient
norm is at most
The series and derivatives
converge normally on compact subintervals. After differentiating
Entire Dirichlet continuation. Here we apply the same finite
differences to
This is summable over the distinct
positive centers. The Dirichlet polynomials of the blocks therefore
converge normally on every compact set and define an entire function. In
Remark 10.9 (Observations that do not determine
irrationality). The following data, taken together, do not determine
whether
Ordinary proof; not formalised in Lean.
Proof. Every constructed sequence has the specified data of
Taking finite linear combinations of the Dirichlet series on arithmetic progressions shows that every fixed periodic twist changes by an entire function. An entire summand has no negative Laurent coefficients: it therefore preserves every pole and its principal part wherever the original series has meromorphic continuation. The regular part and zeros need not be preserved. In the untwisted case the classical identity gives
The version used by Coons [37] supplies this
function identity, not an irrationality theorem for one value of
The change of sign is indispensable for this construction. An
infinitely supported nonnegative integer correction has unbounded Abel
limit at one. The Dirichlet series of the correction also cannot extend
to an entire function if its defining series converges in a right
half-plane. Indeed, choose a positive real
Integer nonnegativity forces finite support, and a finite correction at an integer reciprocal base cannot change rationality. Signed differences are what allow the stronger observation class above.
Remark 10.10 (The first-harmonic test on the rational
members). Let
Ordinary proof; not formalised in Lean.
Proof. The actual tail
This applies to every nonempty subset of the block, including the
actual totient-selected set
Hypotheses of the conditional implications
Uniformity in a parameter does not remove a hypothesis. An implication can hold at every scale although the required arithmetic input is known at only finitely many scales, or at none. We examine that distinction for the displayed implications, without drawing conclusions about all arguments that use the same objects.
Implications concerning the 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 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
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
false_of_compressedAdjointCertificate),
but that calculation does not exclude matrix arguments with different
boundary conditions.
Additional mathematics required by the sufficient conditions
We turn from the proved reductions to the estimates needed to apply them. The doubling identity relates window phases to exact tails; the subsequent decompositions separate the weighted sums for which cancellation is required. The suggested analytic applications remain proposals where those estimates are missing. Failure of one application does not exclude the analytic method.
The section contains a doubling-orbit formulation with explicit
thresholds, a lacunary comparison sequence for the strength of a block
estimate, and sufficient estimates for the prime-factor decomposition.
The discussion of a rank upper bound must also be read with the rational
The proved reductions identify explicit sufficient hypotheses. Those hypotheses remain to be established; the reductions do not prove them.
The doubling identity
Write Erdos249257.TotientTailPeriodKiller.totientTail),
and
Lemma 12.1 (The doubling identity). For all
so
Hence, for fixed
The recurrence
These identities express the phases as a lacunary exponential sum in one real variable. The next proposition transfers an estimate for that orbit to the truncated phases, accounting for the truncation error. The identities themselves are already in the cited sources.
Proposition 12.2 (Transfer to the doubling orbit). Suppose that
This hypothesis implies that
Proof. Fix Erdos249257.TotientTailPeriodKiller.norm_windowFirstExp_sub_tailOrbitFirstExp_lt)
gives Erdos249257.TotientTailPeriodKiller.windowFirstCos_le_add_of_tailOrbitGap),
The proof above makes the truncation margin explicit. The full
implication is also proved in Lean (ErdosProblems.Erdos249.irrational_totient_series_of_tailOrbitBlockGap).
It uses a real-part estimate for the exact phases and spends
Corollary 12.3 (A digit version of the analytic
condition). Let
Proof. The inequality
Proposition 12.2 now
applies. For the digit reading, for a nondyadic
The exact hypothesis is the digit-change inequality in the corollary. It is not a claim about an average run length: the two boundary runs of a finite block need not be complete, and their lengths are not specified by the number of interior digit changes. The finite observations below satisfy the displayed bound at their sampled parameters. They do not establish it on arbitrarily large blocks.
| required | ||||
|---|---|---|---|---|
For the numerical enclosure, compute
The endpoints
have the same quotient on division by
Observation 12.4. Lemma 12.1 expresses each tail phase
in terms of the doubling orbit of
The full-block exponential-sum estimate
The required inequality.
where Erdos249257.TotientTailPeriodKiller.DTWFirstHarmonicNormGap,
Erdos249257.irrational_totient_series_of_first_harmonic_norm_gap).
By Proposition 12.2
the real-part bound with constant
The discrepancy in terms of the doubling map.
For
The phase is a geometrically weighted sum of totients at
Relevant comparison estimates.
The following comparisons identify the estimates still needed; they do not rule out these methods.
Weyl differencing and van der Corput. The van der Corput
inequality applies to arbitrary bounded complex sequences [23], but its use here
requires estimates for shifted correlations. For the exact phases
Thus
differencing gives another doubling orbit, not a polynomial phase of
lower degree. The finite phase
The large sieve. A proposed application would need a
suitable family of separated frequencies and a way to recover a bound
for each fixed
Bilinear sums over prime factors. Factoring
Erdős’s 1948 digit method. The comparison series is
The identity follows by Möbius inversion; a
numerical computation gives
Erdős combines congruences forcing increasing powers of
The unresolved estimate.
For general coefficients
Theorem 12.5 (The block norm condition is stronger in
the class
Consequently the block norm condition
fails for
Proof. The binary expansion of
If
when
To pass from these exact phases to the finite residue test, note that
This example rules out the implication from irrationality and the stated coefficient bound to the block norm condition. It does not say that the totient sum is Liouville-like, or that every argument based on its digits fails. A proof of the block estimate must use information that distinguishes the actual totient phases from this comparison sequence.
The size of the required saving.
Under Lebesgue measure on the phase circle, the binary digit maps are
independent fair bits. The digit-change proportion therefore tends to
The four-term decomposition
The simultaneous inequalities.
Use the four finite sums defined in Section 3.2; in particular, each
group mean averages the selected prime phase, not the residual weight.
For every
Their simultaneous validity remains unproved;
together they imply irrationality (Erdos249257.TotientTailPeriodKiller.DTWPivotResidualDecorrelation,
Erdos249257.irrational_totient_series_of_pivotResidualDecorrelation).
The decomposition is an exact identity (Erdos249257.TotientTailPeriodKiller.windowFirstExp_sum_eq_pivot_decomposition).
The last two sums are bounded by counting indices, since every phase has
modulus one. The mean contribution is bounded by the triangle inequality
once a uniform group-mean estimate is available. The remaining sum
retains a varying weight after centring, and requires a separate
real-part estimate. The parameters Erdos249257.TotientTailPeriodKiller.mem_pivotFiber_one_overlap_iff).
An upper bound for the unassigned terms.
Only an upper bound is needed here. We enclose the unassigned arguments in a set of smooth numbers and count that larger set. There is no claim that every smooth argument is unassigned.
Proposition 12.6 (A one-sided bound for the
unassigned terms). Fix
for all sufficiently large
Proof. Let
The first case also gives
For completeness, the classical fixed-parameter asymptotic
Monotonicity in
The Lean proof uses no smooth-number asymptotic. For large
Mertens’ theorems, proved in Lean with explicit constants, then give
Proposition 12.7 (The excluded-cofactor estimate).
Fix
so a single choice of
Proof. For a fixed cofactor
The
possible endpoint contribution is
Multiplying
the two estimates proves the stated bound. If
The existence of a usable cutoff can also be made explicit by an
elementary estimate. For
The first step uses
The first element of
This finite weighted proportion is not
the limiting density
The growing dyadic modulus.
The selected offset is
On a group with cofactor
Choosing
The remaining prime-weighted correlation.
Propositions 12.6
and 12.7 give the
unassigned and excluded-cofactor bounds at minimal admissible depth.
They must be combined with mean and correlation estimates at the same
With the notation of Section 3.2, the correlation estimate still required is
The sum is over
the assigned indices with good cofactors, not all primes and cofactors
in the interval. By (3),
Regrouping by
A fixed-offset example illustrates the correlation at issue. At
This fixed-offset example is not Definition 3.4: there
Averaging over the block parameter.
For each fixed
where every
The displayed average is a Cesàro average of norms on dyadic blocks. It is not the signed logarithmically weighted correlation appearing in the cited Chowla–Elliott theorems. The position of the absolute value matters: cancellation between different blocks would not bound this sum of norms. Invoking entropy decrement would therefore require an additional argument yielding this particular estimate.
The finite phase depends on the
Separation along prime positions
The quantified prime condition.
This condition is unproved; it implies irrationality (ErdosProblems.Erdos249.DTWNaturalPrimeTailOrbitStrictGap,
ErdosProblems.Erdos249.irrational_totient_series_of_naturalPrimeTailOrbitStrictGap).
Its meaning for the doubling map.
What the prime condition adds.
The preceding condition asks for a separated point at a prime-indexed position. The full-block average does not by itself locate such a point on a prescribed sparse set. Conversely, the prime condition does not assert cancellation over the whole interval. They are different sufficient hypotheses; no general comparison of their difficulty is proved here.
Finite comparison.
Among the
An average over a prescribed prime sample.
The subset implication, Theorem 9.5, allows a nonempty
finite set
For Erdos249257.TotientTailPeriodKiller.mem_pivotFiber_one_overlap_iff).
A sufficient, unproved condition is
The subset theorem then gives a certificate at
some
On this sample the selected cofactor is
Remark 12.8. Fixing the sample rules out the particular argument that selects a pair only after locating separation. It does not prove that (5) is inequivalent to irrationality, or that it is a strictly stronger condition. No such comparison is established here.
Depth equal to a period multiple
The quantified residue condition.
unpacked, ErdosProblems.Erdos249.PeriodMultipleEscape.ApFullDepthEscape,
ErdosProblems.Erdos249.FullDepthRayAmplifier.apFullDepthEscape_iff_irrational);
both directions are proved, and the remaining gap is a nonintegral tail
difference
The condition in terms of binary digits.
Writing Erdos249257.TotientTailPeriodKiller.abs_tail_diff_lt),
applied at
Proposition 12.9.
Proof.
Proposition 12.9
gives a sufficient analytic criterion for the condition with depth equal
to the shift: for each
Comparison with digit complexity.
The phase inequality above is a quantitative statement at specified positions and period multiples. A general block-complexity assertion is a different quantified statement, of the kind treated by the Adamczewski–Bugeaud method for algebraic numbers [27]. No implication from such an assertion to the required inequality is established here. In particular, this record does not justify describing one existing method as the only possible route, or algebraicity as the sole missing input. The arithmetic nonintegrality obligation must be stated and proved in its own right.
Finite examples.
At
A possible heuristic, not an estimate.
If a phase
A rational series with unbounded carry rank
For an integer sequence
do not imply
The limit condition fixes the value of the series. Dividing the
recurrence by
Thus
The comparison with value .
We alter only even coefficients, whose weights are
The interval
Consequently
These are nonnegative
integers: for
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
The same
The rank quantities.
Finite-dimensional span of all dyadic sections is the definition of a
Erdos249257.not_finiteDimensional_span_fullTotientKernel)
proves the case
For a rational-valued sequence
For
integer sequences
Since every section of
In particular, bounded carry ranks would force bounded coefficient
ranks. Non-
The theorem for
Finite observations and quantified conditions
The finite observations can be compared with the quantified conditions, but they do not establish an asymptotic digit distribution. They also supply no basis for ranking possible proof methods.
Comparison of conditions.
The following table records the conditions themselves, rather than sufficient digit proxies. Lemma 12.1 explains how their phases are related.
| Condition | Required assertion | Indices and quantifiers |
|---|---|---|
| Block norm | Norm at most |
All |
| Four terms | The four separate budgets of Definition 3.4 | One common |
| Prime gap | Distance from |
The phase |
| Full depth | |
Every |
| Generic rank bound (false) | A uniform or subexponential upper bound for carries of rational coefficient series | All finite dyadic levels; refuted by
the |
The first four conditions concern the same constant but impose
different averaging, sampling and separation requirements. The
Quantitative estimates.
The counterexamples identify missing assumptions in the specific
arguments tested here. They do not imply that the binary digits of
Additional arithmetic information.
Table 1 records
finite observations: the sampled digit-change proportions are near
The recorded small margins near a forbidden endpoint also require careful interpretation. One small margin disproves a proposed lower bound larger than that margin at that index. It does not rule out every positive margin on a suitable subsequence, or every estimate with scale-dependent bounds. No numerical census in this record determines which of these possibilities holds asymptotically.
Scope of the comparison.
Corollary 12.3
specifies one sufficient digit statistic: for every fixed
Remaining arithmetic questions
The remaining questions ask for witnesses with unbounded indices. We
collect them in residue and exponential-sum form, retaining the
quantifiers needed to imply irrationality of
This section collects quantified conditions on the scaled tail Erdos249257.TotientTailPeriodKiller.totientTail
Each condition is stated with its quantifiers and linked to its formal source. The comparison distinguishes proved equivalences from one-way sufficient conditions. It is not an exhaustive list of possible methods. A finite list of certificates does not stand in for a condition beyond every threshold, and an implication does not establish its antecedent.
Recall that Erdos249257.TotientTailPeriodKiller.periodLcm).
For nonnegative integers
Erdos249257.TotientTailPeriodKiller.windowDiscrepancy
The certificate
Erdos249257.TotientTailPeriodKiller.certifiedKill
This condition is decidable. Thus the least nonnegative residue must lie
more than
Certificate completeness
For each fixed
Erdos249257.TotientTailPeriodKiller.exists_certifiedKill_iff_tail_diff_notMem_int
(The same equivalence is also stated at Erdos249257.totient_tail_window_kill_exists_iff_tail_diff_not_int.)
This equivalence removes the existential depth from the unrestricted certificate conditions below, including the diagonal and LCM-grid forms. It does not by itself supply a depth bound, a prescribed separation margin, a common depth for a family, or an exponential-sum estimate. Such requirements must be retained unless a separate argument removes them. In particular, completeness does not establish any of the quantified nonintegrality assertions needed for irrationality.
The original quantified residue condition
The threshold quantifier excludes every possible starting point for a rational tail period.
The quantified residue condition.
Here Erdos249257.TotientTailPeriodKiller.irrational_totient_series_iff_certificate_supply
The equivalence is proved; the quantified existence assertion is not
proved.
The reverse direction is by contradiction against the tail-period
law: if Erdos249257.TotientTailPeriodKiller.eventual_period_of_not_irrational,
unconditional) supplies a period Erdos249257.TotientTailPeriodKiller.tail_diff_notMem_int_of_certifiedKill).
For the forward direction, irrationality gives pointwise
non-integrality of every positive tail shift and certificate
completeness supplies a witness already at
For fixed
Multiples, diagonals, and LCM grids
Completeness allows the irrationality question to be expressed using multiples of a period, diagonal tails or an LCM grid. The implications below prove these equivalences. Each formulation permits a different estimate to be attempted, but none supplies the witnesses it requires.
Multiples of a period.
Erdos249257.TotientTailPeriodKiller.irrational_totient_series_of_multiple_certificate_supply
The preceding residue condition implies this one by taking
The diagonal.
Erdos249257.TotientTailPeriodKiller.irrational_totient_series_iff_lcm_diagonal_certificate_supply
The two parameters in a hypothetical rational tail period are
absorbed by one LCM index. For Erdos249257.TotientTailPeriodKiller.irrational_totient_series_of_lcm_certificate_supply).
Conversely, irrationality and pointwise completeness give a diagonal
certificate already at
The finite assertion ErdosProblems.Skip.LadderT67.exists_diagonalKill_le_82).
The historical list contained 28 explicit values through Erdos249257.TotientTailPeriodKiller.certifiedKill_diagonal_all_imported;
endpoint Erdos249257.TotientTailPeriodKiller.certifiedKill_diagonal_t64).
These are finite computations. The current contiguous range is still
finite and does not establish witnesses at arbitrarily large indices; no
certificate at
The LCM grid.
Erdos249257.irrational_totient_series_of_lcm_cone_window_kill_supply
The diagonal choice is Erdos249257.rational_totient_series_forces_lcm_cone_flatness).
A certificate for any such difference is a contradiction.
The finite-grid condition of Theorem 6.56 offers a second
test. At
For every
threshold Erdos249257.irrational_totient_series_of_lcm_cone_nonflat_supply).
The modulus bound is one-sided at each point; it does not imply a
factor-of-two reduction in the number of binary digits.
Equivalent nonintegrality statements
Via the completeness iff above, the diagonal and cone forms restate,
exactly, with no reference to
Erdos249257.irrational_totient_series_of_lcm_diagonal_nonintegrality_supply
(cone analogue at Erdos249257.irrational_totient_series_of_lcm_cone_nonintegrality_supply)
Thus one can ask directly whether
The block exponential-sum condition
A bound for an exponential sum is sufficient for the quantified
residue condition. With
Erdos249257.TotientTailPeriodKiller.DTWFirstHarmonicNormGap
The universally quantified assertion is not proved.
Erdos249257.TotientTailPeriodKiller.irrational_totient_series_of_first_harmonic_norm_gap
The threshold is
The underlying finite lemma is more general: it applies to any
nonempty finite Erdos249257.TotientTailPeriodKiller.exists_certifiedKill_of_first_harmonic_norm_gap)
uses the elementary block lemma of Theorem 9.4, which is
unconditional as an implication. The real-part version uses
What supplying this form would take: genuine cancellation
for the additive character Erdos249257.ResidualGaugeObstruction.det_residualMonomialMatrix)
gives a comparison in which every weighted phase equals
The actual tail difference on the LCM diagonal
For
The exact equivalence.
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.irrational_totientSeries_iff_actualLcmOrbitNonintegralitySupply
This is an unconditional equivalence, where Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.actualLcmTailOrbit_eq_scaled_totientSeries_sub_prefix).
The right-hand side is an equivalent reformulation of irrationality, not
a weaker hypothesis already established by the finite examples. The
following sufficient conditions are attempts to prove it.
An impossible complete divisibility pattern
Let
It is impossible that
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.not_actualLcmTerminalDyadicStaircase_of_room
Indeed, the last requirement would make
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.lcmRayArithmeticLetter_pos_of_lt_two_mul,
without a rationality hypothesis.
Omitting only the last divisibility requirement leaves the partial
pattern in Proposition 6.86. It additionally
requires
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.puncturedDyadicStaircase_penultimate_eq_half
The terminal difference is not pinned to
The remaining upper-endpoint residue
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.ActualLcmTopEdgeResidueGap
No unbounded family satisfying this condition is known.
The positivity theorem gives
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.actualLcmTailDiff_shift_pos
For
Hence, when Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.actualLcm_integral_forces_topEdgeResidue).
More generally, the bounds
because
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.actualLcmTailDiff_notMem_int_of_topEdgeResidueGap
The one-sided inequality excludes the upper-endpoint interval forced by
integrality. Positivity alone does not establish that inequality.
The cofinal target built from it is
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.PowerTwoActualLcmTopEdgeResidueGapSupply
This condition is unproved; its implication is proved:
Five sufficient conditions for that residue inequality
The next five quantified conditions each imply irrationality. Conditions (i)–(iv) reach the upper-endpoint test; (v) gives nonintegrality directly. Their proven relations are summarised in Proposition 6.65.
For every
, there are and with such thatwhere
. The size condition includes the larger depth , so the conclusion remains valid whichever of the two adjacent depths gives the certificate. This condition is unproved (Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.PowerTwoAdjacentSuffixMidbandSupply); its sufficiency is proved (Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.powerTwoActualLcmTopEdgeResidueGapSupply_of_adjacentSuffixMidband,Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.irrational_totientSeries_of_adjacentSuffixMidbandSupply).For every
, there is with the following property. Put and choose so that is the least odd integer not smaller than . Define integers recursively byThe increments
are even, so the recurrence is integral. The required inequality isAt depth
, the residue in (i) equals . Dividing its two endpoint bounds by and using integrality gives exactly the threshold . This condition is unproved (Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.PowerTwoOddGuardTopEdgeHalfWordBandSupply). The width is and the depth is the prescribed depth; both must be retained when comparing this with a fixed-fraction band. Its sufficiency is proved (Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.powerTwoAdjacentSuffixMidbandSupply_of_oddGuardTopEdgeHalfWordBand).Use exactly the quantifiers and prescribed depth of (ii). Let
and define its centred representative byThus
; when a midpoint occurs, the positive representative is used. The equivalent inequality isThis condition is unproved (
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.PowerTwoActualFinalTopEdgeMagnitudeSupply). At the prescribed depth the size bound holds. For a residue in , the band in (ii) is therefore exactly this absolute-value condition. The equivalence, including its quantifiers, is proved (Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.topEdgeHalfWordBandSupply_iff_actualFinalCenteredMagnitudeSupply).Allow the odd depth to vary, but retain both size bounds. For every
, require and withThis condition is unproved (
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.PowerTwoFlexibleActualTopEdgeMagnitudeSupply). The first bound keeps the adjacent depth inside the short window; the second makes the required residue band nonempty. One implication passes through (i), and another gives the two-sided carry exclusion below (Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.powerTwoAdjacentSuffixMidbandSupply_of_flexibleActualTopEdgeMagnitude,Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.irrational_totientSeries_of_flexibleActualTopEdgeMagnitudeSupply).Retain the full quantifiers and the two size bounds in (iv), but replace its absolute-value inequality by
This compares the signed centred residue with the terminal totient difference. It is not an unrestricted assertion at an arbitrary
. This condition is unproved (Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.PowerTwoFlexibleActualTerminalDominanceSupply); its sufficiency is proved (Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.irrational_totientSeries_of_flexibleActualTerminalDominanceSupply).
A further sufficient terminal-carry condition
With
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.PowerTwoFlexibleActualTerminalCarryCorridorEscapeSupply
Either alternative gives nonintegrality at that scale, so the quantified
condition implies irrationality (Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.irrational_totientSeries_of_flexibleActualTerminalCarryCorridorEscapeSupply).
The proof assumes an integer
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.two_mul_actualOddHalfCenteredLift_eq_terminal_sub_trueCarry
The carry is then a positive tail difference, strictly smaller than
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.actualLcm_trueEndpointSurvivor_neg).
The first alternative contradicts the upper bound; the second
contradicts positivity, which is the terminal-dominance argument (Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.actualLcmTailOrbit_notMem_int_of_actualTerminalDominance).
Both arguments are conditional contradictions, not evidence against either unproved estimate. No converse from nonintegrality to either finite inequality is asserted. In particular, the exact identity must not be described as making this sufficient condition necessary.
Certificates in short windows
For every
No coprimality restriction on Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.lcmRayArithmeticLetter_eq_deltaTotient).
Consequently the corresponding window numerator is
and applying the same residue and error bounds gives precisely the test
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.lcmDiagonalArithmeticKill_iff_certifiedKill).
Thus the quantified assertion
implies irrationality (Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.PowerTwoActualLcmShortArithmeticKillSupply,
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.actualLcmOrbitNonintegralitySupply_of_shortArithmeticKill);
the assertion itself is unproved. It restricts the diagonal indices to
powers of two and imposes the additional bound
The displayed certified examples have Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.actualLcmTailOrbit_four_and_six_notMem_int);
these are finite computations. The bounded statement of Theorem 9.22
uses the single witness
A sufficient approximation bound
Put
For every
Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.abs_actualLcmTailOrbit_sub_rawApprox_lt
Let
This
condition is unproved; its sufficiency is proved (Erdos249257.DiagonalFreshLossBridge.PowerTwoOddWindowAffine.irrational_totientSeries_of_actualLcmOrbitSeparationSupply).
The triangle inequality then gives
An equivalent test using two leading residue bits
Proposition 6.87
gives an equivalent certificate condition: there are
Erdos249257.TotientTailPeriodKiller.exists_certifiedKill_iff_guardCylinderWitness
The forward proof selects
Farey growth and the failed generic rank argument
The Farey growth law is an open sufficient hypothesis. The generic rank bound listed beside it is false for rational comparison sequences, and is retained to explain that failed input rather than as another open problem.
The hypothetical rank bound.
Unconditionally, for every level Erdos249257.linearIndependent_canonicalTotientKernelFamily).
Consequently, if
It obeys Erdos249257.not_irrational_totientSeries_implies_unbounded_carryRank_unconditional
A bound independent of
The most direct generic construction is also impossible: no integer
certificate satisfying the following conditions (Erdos249257.false_of_compressedAdjointCertificate);
and the full family is proved infinite-dimensional in span, the case
Erdos249257.not_finiteDimensional_span_fullTotientKernel).
Proposition 1.7 gives a common
eventual period modulo
Growth of the Farey denominator bound.
The finite denominator exclusion for
Erdos249257.tsum_totient_div_pow_two_ne_ratCast_of_den_le_79639646646701375323355774875831053
This bound is sharp at GapFareyBound.gap_check_window_1_240_first_failure);
so the same interval cannot exclude every rational at the next
denominator. A different window requires a new certificate or a uniform
argument; the fixed-window calculation supplies neither.
A sufficient extension is a function
For Erdos249257.reducedDenominatorCandidateCount_prime_pow_le_one).
The success hypothesis is essential: the bound is not a statement about
every window at that denominator. Nor does it bound the eventual
denominator cutoff. The prime-power restriction cannot be omitted, as
the modulo-
Summary of implications
For each condition, the second column states its relation to the quantified residue test or to the named intermediate assertion.
Reading the table. “Sufficient” records only the indicated
implication. It does not assert a converse or a strict comparison of
strength. “Equivalent” records two proved directions, either directly or
through the base equivalence with
Remaining estimates
Two explicit estimates for
Exponential sums.
For each fixed
The saving
The last totient difference.
The endpoint criteria compare
with
twice the centred residue
Complementary proofs for the short paper
The basis
theorem, the integral
relation theorem and the bounded
residue theorem have complete proofs in the short paper. This
appendix supplies the longer arguments behind its discussion of
Propagation of nonintegral tail differences
Write
The identity
has an integer finite sum. Subtracting the identities at
In particular, a nonintegral tail difference
excludes every rational value whose denominator divides
The finite test.
For
All residues below are least nonnegative
residues. Write
The omitted terms form another difference of scaled tails:
Since
If
Theorem A.1 (Propagation of one nonintegral tail
difference). Fix
Requiring this for every
Unrestricted completeness cannot simply set
Proof. Set
If the test also fails at
The recurrence has transferred
two shrinking errors to the same fixed number
Finally, (6) is
nonintegral for every
For instance
This enclosure proves nonintegrality without
evaluating the infinite tails. The theorem gives infinitely many
certificates with depth equal to the shift for this pair, not for every
Residues modulo divisors of Mersenne numbers
Fix a hypothetical denominator
an integer
modulus and an integer prefix, respectively. The test below asks whether
the residue of
Equivalent formulation A.2 (A residue test modulo a
divisor of
Proof. The identity
is exact. For
If
For fixed
A formal declaration for the equivalence is available
here, with the modulus written as
which is an exact recurrence for searches directed at (8).
LCM tails and rational comparisons
We first specialise the tail congruence to LCM shifts, then compare it with rational series preserving selected coefficient data. The source declarations accompany the formulas; references point to the complete constructions and their hypotheses in the preceding sections.
Tail differences at least common multiples. Let
. Then is irrational if and only if, beyond every threshold , some satisfies . This is the exact cofinal nonintegrality criterion for the actual LCM diagonal, not a quantitative separation estimate and not a proof that such indices occur; the forward implication is recorded separately.Positive tail differences need not be nonintegral. For
and , one has . Suppose this difference is an integer. If a truncation depth satisfiesthen
lies strictly between
and . The later tail difference is a positive integer; its negative is the representative near zero. Thus positivity determines which endpoint contains the residue, but does not exclude an integral tail difference. Both displayed bounds on are required for this conclusion. Source declarations: positive tail differences, negative endpoint representative, residue near the upper endpoint.Divisibility and finite linear combinations do not suffice. A dyadic coboundary is a sequence of the form
; its weighted sum telescopes. For every , with , the linked source constructs a nonzero comparison sequence of this form. Its coefficients reproduce the actual totient differences at prescribed indices and are divisible by . Every finite integer linear combination of forward shifts preserves the telescoping identity and divisibility by and the corresponding lower-level factors. The bounds remain uniform in the index, but are multiplied by the sum of the absolute values of the combination’s coefficients. A variant preserves sparse prescribed values along entire arithmetic progressions. These properties alone do not force a contradiction: the comparison need not consist of actual totient differences. The theorem concerns linear combinations of shifts, not nonlinear operations, and does not supply certificates at arbitrarily large scales. Source declarations: obstruction for finite integer combinations of shifts.
If
In particular
Section 12.6 constructs a
rational comparison sequence with
This
comparison sequence has an integral carry satisfying
The sharp rank-one quotient bound
The quotients below are a particular proposed family of rational approximants to a Möbius-weighted value. We determine their minimum and show that they remain a fixed distance above that value. Put
The divisor-convolution
identity
Theorem A.3 (A lower bound for the rank-one
quotients). For
The
uniform bound
Proof. We first bound every denominator away from zero. We
then compare
Since
For
For the
strict upper bound, the tail bound is smaller than
Write
For
Each comparison follows by multiplication by
positive denominators. The first left-hand side bounds every quotient in
its range from below. So does the last, by the tail estimates with
It remains to compare the minimum with
The exact prefixes are
Comparison of fractions gives
The minimum
proves the lower gap for every quotient; the second inequality proves
failure of the proposed
This theorem treats averages after the quotients are formed. Signed
coefficients, coupling before the quotient, and higher-rank kernels
require separate arguments. For rational approximants
The denominator sets the scale of the required error. Convergence alone
does not control their product. For the elementary dyadic prefixes, the
available bound is only
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
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
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;
Möbius identities and rational approximation.
unique
minimizer; uniform
lower bound
Proposed exponential-sum and prime-factor estimates.
window-separated
pairs; the
unproved quantitative separation condition at primes; a
positive adaptive truncation budget;
Declarations
Further background.
Erick Wong posted a proof that
At the generating-function level, the published height criterion of
Adamczewski, Bell and Smertnig gives
Automatic prime-sampling theorems address a different issue. Adamczewski, Drmota and Müllner identify a computable local coprimality condition governing the relevant logarithmic densities, with a conditional ordinary-density transfer [34]. Their theorem does not assert that every output state has positive density on a prescribed prime progression, nor does it prove independence with automatic coefficient weights. Any use for that purpose needs its own compatibility argument.
Sources and data.
The evidence record lists every Lean declaration, version and check behind the margin marks.
Verification scope.
Kernel checking validates a formal proof of its stated proposition relative to the declared axioms. It does not check that every prose summary has the same hypotheses or verify the literature comparisons. In particular, a checked implication with an unproved hypothesis is not a proof that Problem 249 is solved.
Funding and competing interests.
This work received no external funding. The author declares no competing interests.
References
J.-P. Allouche and J. Shallit, The ring of
-regular sequences, Theoret. Comput. Sci. 98 (1992), no. 2, 163–197, doi:10.1016/0304-3975(92)90001-V. Definitions and early statements are cited with the author preprint’s numbering.M. Coons, (Non)Automaticity of number theoretic functions, J. Théor. Nombres Bordeaux 22 (2010), no. 2, 339–352, doi:10.5802/jtnb.718. Theorem 3.2, p. 348.
M. Coons, Regular sequences and the joint spectral radius, Internat. J. Found. Comput. Sci. 28 (2017), no. 2, 135–140, doi:10.1142/S0129054117500095; arXiv:1511.07535v1. Theorem 1, Proposition 4 and Corollary 7 are cited with the arXiv v1 numbering.
G. Martin, Simultaneous inequalities among values of the Euler phi-function, arXiv:math/0603053v1, 2006. Theorem 1, pp. 1–2.
E. Wong, answer 1211557 to An infinite sum based on the mod-parity of Euler’s totient function, Mathematics Stack Exchange, 29 March 2015, accessed 15 September 2026.
P. Erdős, On the irrationality of certain series, Indag. Math. 19 (1957), 212–219, https://users.renyi.hu/~p_erdos/1957-07.pdf. Lemma 1, p. 213; Lemma 4, pp. 215–218; Lemma 4
, p. 218.H. Kaneko, Y. Suzuki and Y. Tachiya, Refinements of Erdős’s irrationality criterion for certain sparse infinite series, arXiv:2601.20743v1, 2026. Theorem A, p. 2; Theorem 3, p. 5; proof of Theorem A, p. 18.
A. Eldar, comment and formula added to OEIS A256936 (revisions 28 and 31), 15 March 2026, https://oeis.org/history?seq=A256936, accessed 16 September 2026.
S. Fan, comment on Erdős Problem #249, 16 May 2026, 19:01, Erdős Problems discussion thread, accessed 16 September 2026.
P. Erdős and R. L. Graham, Old and New Problems and Results in Combinatorial Number Theory, Monographies de L’Enseignement Mathématique 28, 1980, p. 61.
P. Erdős, On arithmetical properties of Lambert series, J. Indian Math. Soc. (N.S.) 12 (1948), 63–66, https://users.renyi.hu/~p_erdos/1948-04.pdf.
K. Postelmans and W. Van Assche, Irrationality of
and , J. Number Theory 126 (2007), no. 1, 119–154, doi:10.1016/j.jnt.2006.11.011; arXiv:math/0604312v1. Theorem 1.3 is cited with the arXiv v1 pagination, p. 3.Yu. V. Nesterenko, Modular functions and transcendence questions, Sb. Math. 187 (1996), no. 9, 1319–1348, doi:10.1070/SM1996v187n09ABEH000158. Corollary 2, p. 1320.
W. Schramm, The Fourier transform of functions of the greatest common divisor, Integers 8 (2008), #A50, https://math.colgate.edu/~integers/i50/i50.pdf. Theorem and equation (2), p. 2.
L. Tóth, A survey of gcd-sum functions, J. Integer Seq. 13 (2010), Article 10.8.1, https://cs.uwaterloo.ca/journals/JIS/VOL13/Toth/toth10.pdf. §1, equations (1)–(2).
M. Merca and M. D. Schmidt, Generating special arithmetic functions by Lambert series factorizations, Contrib. Discrete Math. 14 (2019), no. 1, 31–45, doi:10.55016/ojs/cdm.v14i1.62425; arXiv:1706.00393v2. Equation (1) is cited with the arXiv v2 pagination, p. 2.
M. Merca, The Lambert series factorization theorem, Ramanujan J. 44 (2017), 417–435, doi:10.1007/s11139-016-9856-3. Theorem 1.2, p. 420.
V. Kovač and T. Tao, On several irrationality problems for Ahmes series, Acta Math. Hungar. 175 (2025), no. 2, 572–608, doi:10.1007/s10474-025-01528-0; arXiv:2406.17593v4. Theorem 2.3 is cited with the arXiv v4 pagination, p. 5.
R. Balasubramanian, S. Giri and P. Srivastav, On correlations of certain multiplicative functions, J. Number Theory 174 (2017), 221–238, doi:10.1016/j.jnt.2016.10.001; arXiv:1511.02221v3. Theorem 2.2 is cited with the arXiv v3 pagination, p. 2.
A. Granville, Smooth numbers: computational number theory and beyond, in Algorithmic Number Theory, MSRI Publ. 44 (2008), 267–323, https://library.slmath.org/books/Book44/files/09andrew.pdf. Equations (1.1) and (1.3), p. 268.
I. Schoenberg, Über die asymptotische Verteilung reeller Zahlen mod 1, Math. Z. 28 (1928), 171–199, doi:10.1007/BF01181156. §17, p. 193, for the distribution of
.I. J. Schoenberg, On asymptotic distributions of arithmetical functions, Trans. Amer. Math. Soc. 39 (1936), no. 2, 315–330. Theorem 1, pp. 318–319; §8, p. 323.
N. Edeko, H. Kreidler and R. Nagel, A dynamical proof of the van der Corput inequality, Dyn. Syst. 37 (2022), no. 4, 648–665, doi:10.1080/14689367.2022.2100244; arXiv:2106.11835v3. Theorem 2.1 is cited with the arXiv v3 pagination, p. 4.
K. Matomäki and M. Radziwiłł, Multiplicative functions in short intervals, Ann. of Math. 183 (2016), no. 3, 1015–1056, doi:10.4007/annals.2016.183.3.6; arXiv:1501.04585v4. Theorem 1 is cited with the arXiv v4 pagination, pp. 1–2.
T. Tao, The logarithmically averaged Chowla and Elliott conjectures for two-point correlations, Forum Math. Pi 4 (2016), e8, doi:10.1017/fmp.2016.6; arXiv:1509.05422v4. Theorems 1.2–1.3 are cited with the arXiv v4 pagination, pp. 2 and 5.
T. Tao and J. Teräväinen, Odd order cases of the logarithmically averaged Chowla conjecture, J. Théor. Nombres Bordeaux 30 (2018), no. 3, 997–1015, doi:10.5802/jtnb.1062; arXiv:1710.02112v1. Theorem 1.1 is cited with the arXiv v1 pagination, p. 2.
B. Adamczewski and Y. Bugeaud, On the complexity of algebraic numbers I. Expansions in integer bases, Ann. of Math. 165 (2007), no. 2, 547–565. Theorem 1, p. 549.
G. Everest, A. J. van der Poorten, Y. Puri and T. Ward, Integer sequences and periodic points, J. Integer Seq. 5 (2002), Article 02.2.3. Lemma 3.1 is cited with the preprint pagination, p. 5.
P. Erdős and I. S. Gál, On the law of the iterated logarithm. I, Proc. Kon. Ned. Akad. Wetensch. Ser. A 58
Indag. Math. 17 (1955), 65–76, https://www.renyi.hu/~p_erdos/1955-06.pdf.S. Yazdani, Multiplicative functions and
-automatic sequences, J. Théor. Nombres Bordeaux 13 (2001), no. 2, 651–658, https://www.numdam.org/item/JTNB_2001__13_2_651_0/. Theorem 2 and its proof, pp. 652–653; Corollary 4, p. 654.J.-P. Allouche, J. Shallit and R. Yassawi, How to prove that a sequence is not automatic, Exposition. Math. 40 (2022), no. 1, 1–22, doi:10.1016/j.exmath.2021.08.001; arXiv:2104.13072v1. Theorem and example numbering follows the arXiv v1 (2021).
J. Bell and D. Smertnig, Mahler series with multiplicative coefficient sequences, arXiv:2603.23456v1, 24 March 2026, preprint. Theorem 1.3, p. 2; Lemma 3.3, p. 9.
J. P. Bell, N. Bruin and M. Coons, Transcendence of generating functions whose coefficients are multiplicative, Trans. Amer. Math. Soc. 364 (2012), no. 2, 933–959, doi:10.1090/S0002-9947-2011-05479-6; arXiv:1003.2221v2. Theorems 1.5–1.6 are cited with the arXiv v2 pagination, p. 2.
B. Adamczewski, M. Drmota and C. Müllner, (Logarithmic) densities for automatic sequences along primes and squares, Trans. Amer. Math. Soc. 375 (2022), no. 1, 455–499, doi:10.1090/tran/8476; arXiv:2009.14773v2. Theorem 1.4 and Remark 1.5, p. 4, and the proof at the end of Section 7, p. 19, refer to the arXiv v2 (2021).
B. Adamczewski, J. Bell and D. Smertnig, A height gap theorem for coefficients of Mahler functions, J. Eur. Math. Soc. 25 (2023), no. 7, 2525–2571, doi:10.4171/JEMS/1244. Theorem 1.2(b), p. 2528; logarithmic height in Section 1.1.1, p. 2527.
T. Crmarić and V. Kovač, On the irrationality of certain super-polynomially decaying series, arXiv:2504.18712v1 (2025), Lemma 4(a) and Remark 5.
M. Coons, (Non)Automaticity of number theoretic functions, arXiv:0810.3709v3, Theorem 3.3. This version’s numbering differs from the journal version cited above.
K. Habiro, Cyclotomic completions of polynomial rings, Publ. Res. Inst. Math. Sci. 40 (2004), 1127–1146, Theorem 5.2, p. 1138.