Introduction
For an integer
Part I gives the support theorems and the proofs followed by the short paper, Irrationality criteria for Lambert subseries. The subsequent parts concern a different question: whether a prescribed rational number belongs to the Mersenne achievement set. The finite identities in Sections 5–8 describe the integer quotients and their relation to the real greedy sequence. Sections 9–12 state the additional uniform or unbounded-depth assertions needed to apply them. Notation specific to a recurrence is introduced with that recurrence.
Section 13 returns to the support criteria. A logarithmic divisor cost cannot uniformly replace the fractional-cover cost when sampling on multiples of a prescribed modulus, even over complete periods. We prove the counterexample and an initial-interval estimate that survives it.
None of these arguments decides the universal problem,
half-membership or
Notation used throughout
For
At base two write
The greedy support
The finite quotient arguments use
For
The maximum matters: subtraction in the corresponding natural-number source definition is truncated at zero. Statements that remove the maximum establish nonnegativity first.
The integer carry for a support omitting
Some finite-depth statements
use
I. Support theorems and their proofs
Support criteria and their proofs
Reciprocal summability lets us average with a fixed modulus and then enlarge that modulus. We begin with this proof of the extension stated by Erdős. For the weighted and cover criteria the estimates must instead remain controlled on a finite window as the modulus grows. That common-window estimate is what permits the two conditions to be used together.
Reciprocal-summable supports
For every infinite set
is
irrational at every integer base
We show that rationality would impose a positive lower bound and then
construct smaller values. For a positive integer
shows that
The integer sum is
finite, since
Put
To interchange this
limit with the sum over the support, expand
With
Now choose
Consequently the limiting
mean of
We increased the observation length with
A weighted condition on the support
A prime-power factor can compensate for a large sum of reciprocals of
cofactors. If
Theorem 1.1 (A weighted summability criterion).
Let
where
then
is irrational. More precisely, for
for every
Examples and limits of the hypothesis.
Squares, powers of two and factorials satisfy reciprocal summability
and therefore satisfy the base-two weighted condition. Full support does
not: for any fixed finite prime set
Writing
where
Write
Thus
Since
Proof. We first derive the lower bound implied by
rationality and then estimate a finite average of the same quantities.
Division of
Consequently
The integer sum is finite. For
We therefore seek positive indices at which the displacement is arbitrarily small.
Put
Then
Complete periods and at most one incomplete period therefore give
The complete-period term explains the weight in
(1):
replacing
The part of the support beyond the observation range has a uniform
bound. If
and therefore
The incomplete-period term in (4) has
no factor
Indeed, for each fixed
Only finitely many terms occur on the left, so no infinite interchange is hidden here.
We now choose the modulus to be divisible by a fixed finite subset of
the support and by all powers of primes in
and put
Then
Consider first
The first term is bounded using (7).
For
we used
Let
Combining (5), (8), and (9) gives
Increasing the number
and average (10)
over
The resulting finite average satisfies
As
Consequently
The construction is valid for every
positive
Since
Averaging antecedents.
Both averaging proofs in this section end by choosing a term no
larger than a finite mean. Duverney
and Tachiya choose their index in the same way in their refinement
of the Chowla–Erdős method: they average a local coefficient mass over
an arithmetic progression built by the Chinese remainder theorem, and a
term attaining the minimum supplies the bounds that control the tail
beyond it (Section 2, (2.3)–(2.9), pp. 5–6 of the author preprint). Kaneko, Suzuki and Tachiya
measure the average decay of scaled tails by
is at least
Dependence on the chosen primes
The weighted condition need not single out one required prime. We
construct a support for which convergence depends on a prescribed
upward-closed condition on the chosen primes. This description holds at
every integer base. We also allow the empty prime set, with
Proposition 1.2 (realising finite monotone witness
rules). Let
Moreover
Proof. For each nonempty
and let
Let
For example, require the chosen prime set to contain at least two of
A finite estimate on common observation scales
A divisor majorant becomes a sum of geometric tails, one for each
divisor. The positive offsets
The cover argument raises a
base-two tail to a fractional power
For
To read this as sampling, first
choose
The finite estimate
equivalently bounds
Fix
Across dyadic lengths
satisfying
When
Finally, at most one dyadic length satisfies
The first inequality follows from
convexity of
Positive divisor majorants
For a finite set
Indeed,
conditional on
Theorem 1.3 (A summable family of divisor majorants).
For each
Set
then
Every finite set admits such a majorant: take
Proof. Write
The choice
The last identity sums a geometric progression in each residue class. The geometric-series identity also gives
For the first
Fix
This is possible since
The positive lower bound under rationality excludes a rational value at
base two. For
The same proof permits any positive weights
Combining the two support criteria
Separate sequences of small weighted and covered displacements would not give a small sum: their small values could occur on disjoint sets of indices. Instead, the weighted proof chooses one finite distribution and the explicit modulus dependence in (13) lets the cover estimate use that same distribution. We add the two nonnegative errors there and choose an index only afterwards.
Theorem 1.4 (mixed weighted and cover supports).
Let
Proof. Fix
Choose a finite
We use
for sufficiently large
because
Choose a sampled
The inequality also holds when
Why the mixed criterion is strict.
Take an infinite support
The positive-weight variant of Theorem 1.3,
with its hereditary all-base conclusion, also has a kernel-checked
Lean proof. Theorem 1.4 alone does
not exhibit a support outside both individual classes; the preceding
strictness argument also uses the two separating constructions.
Existence of two sets with those properties has a Lean
proof whose second set is formed from squarefree divisor sets with a
different choice of parameters. The printed fresh-prime construction and
the strictness corollary have ordinary proofs, and none of these
constructions has been independently reviewed. The second set in the
Lean proof also admits no cover with
Supports satisfying the mixed criterion are closed under finite
unions and finite changes, even with the fixed dyadic cover cost in
(14).
For two covers, interleave their
The elementary independence boundary.
For the divisor counts
The universal problem and the half-value question
For an integer
Definition 1.5 (Universal #257, written (U)). Is
Definition 1.6 (The half-value question, written (H)).
Let the Mersenne achievement set be mersenneAchievementSet).
Is
A representation of positiveMersenneSupportValue_coe_finset_ne_half).
Hence a witness to
The reciprocal-summable and finite-prime weighted theorems, together with the checked support theorems below, leave (U) and (H) open. The later countermodels identify the particular arithmetic information lost by individual approaches; they do not prove that all such failures have one common cause.
Known support theorems
Full-support irrationality is Erdős’s theorem [1]. The pairwise-coprime case is Erdős’s theorem of 1968, where he also stated that the coprimality condition can be removed [2]. Luca and Tachiya proved irrationality for every purely periodic integer weight that is not identically zero [3]; the purely periodic, eventually periodic, residue-class, odd-support and periodic-weight rows below follow from their theorem, and odd support is their Example 2 [3]. The lcm-gap supports, including factorials and powers of two, have summable reciprocals, as the calculation following the table shows. They are consequently included in the reciprocal-summable theorem stated by Erdős. The final column locates the corresponding declarations.
The two kinds of argument in the table use different data:
divisibility of blocks of
| Support class | Exact hypotheses | Formal proof |
|---|---|---|
| Full support |
irrational_erdosSum_full_support |
|
| Multiples |
irrational_erdosSupportSeries_multiples |
|
| Purely periodic | irrational_erdosSupportSeries_periodic |
|
| Eventually periodic | irrational_erdosSupportSeries_eventuallyPeriodic |
|
| Residue class | any |
irrational_erdosSupportSeries_residueClass |
| Odd support (density |
irrational_erdosSupportSeries_odd |
|
| Growing lcm gap | irrational_erdosSum_of_lcm_gap |
|
| Factorials; powers of two | instances of the lcm-gap theorem | irrational_erdosSum_factorial_support,
irrational_erdosSum_two_pow_support |
| Pairwise coprime (Erdős 1968) | irrational_erdosSupportSeries_pairwise_coprime |
|
| Signed periodic weights | periodic integer weights; their divisor-transformed coefficients are nonnegative and frequently nonzero | irrational_intWeightedErdosSeries_periodic_of_coeff_nonneg_of_frequently_ne_zero |
The lcm-gap hypothesis does imply reciprocal summability. Eventually
For
A separate conditional result allows common factors confined to
divisors of one fixed integer irrational_erdosSupportSeries_of_orthogonalPetalBouquet).
It also assumes that for every
Thus relaxing coprimality does not remove the simultaneous divisibility and tail-bound requirement. This additional hypothesis is not proved here, and the source file does not establish a dichotomy for arbitrary supports.
The record also gives a logarithmic bound on runs of zero divisor
counts under rationality: for each supportCoeffZeroWindow_length_le_eps_logb).
For these supports there is already a simpler unconditional bound. If
shifted_state_unbounded_of_infinite_support
also requires interpretation: an unbounded sequence can still satisfy
Remark 1.7 (What is and is not covered in the universal
direction). The Lean sources contain no theorem for sorry. It is statement-level prior art, and no theorem
recorded here is derived from it. This record has no general theorem for
an arbitrary positive-density nonperiodic or divisor-dense support, and
the universal statement remains open.
Periodic weights: the two hypothesis sets.
The periodic sequence theorem belongs to Luca and Tachiya [14]; their
later author-written account states it as Theorem A [3]. In the displayed
Lean row above, nonnegativity and frequent nonvanishing are assumptions
on
A separate denominator-growth criterion.
Erdős’s growth theorem [21], as restated and recovered by Barreto,
Kang, Kim, Kovač and Zhang [22], gives irrationality of
Indeed
The two hypotheses can be separated explicitly. The squares
Geometry and rational-target membership
At the first differing digit,
Theorem 1.8 (Achievement-set geometry).
Theorem 1.9 (Support-restricted refinement). Use
zero-based indices in this statement: coordinate
Hausdorff dimension of a restricted set.
For example, retaining the positive exponents
Then
Write
The unique Mersenne digit coding therefore defines a map from
The
Remark 1.10 (Achievement-set terminology and sources). We use
the modern term achievement set for the subsum set that Kakeya’s 1914
note describes as a set of partial sums. For an infinite summable
sequence of positive terms, Kakeya proves perfectness, and nowhere
density under an all-index strict-tail condition; Kovač–Tao, Remark 4.1
verifies that strict-tail condition for the fixed-base Mersenne weights.
Nitecki proves that a subsum set whose terms all exceed their tails is a
Cantor set of measure
Theorem 1.11 (Membership equals greedy survival; the
fatal-gap dichotomy). For a real target
For
every
Two boundary degeneracies are excluded at every rank,
unconditionally:
The following finite checks use exact integer arithmetic. Each has a
published
program and saved result, including the scan to row
Independently, rows
Sharp tail margin, ranks
A further exact finite computation, not used in the arguments here,
regenerates the forced half-prefix support to depth seamUpperResetDyadicBandEscape_through_thirty).
Remark 1.12 (Literature, exactly). 11
occurs infinitely often in the binary expansion of
The digit results concern particular patterns. An
irrationality-measure bound controls lengths: a run of
II. Limitations and extensions of recorded methods
Limitations of the recorded methods
A bound for the actual greedy sequence and a bound uniform over a class of supports are different assertions. The following examples separate those assertions, starting with uniqueness at a fixed target. They exclude the specified estimates or their proposed uniformity, without giving an obstruction to every possible method.
What the obstructions do and do not show
We begin with uniqueness at a fixed target and depth, then compare the quantifiers required by the different estimates. The counterexamples identify a failed hypothesis or a missing uniformity, while the equivalences retain the full difficulty of their target statements.
Observation 2.1 (Uniqueness within the fixed-target coding).
Each Mersenne weight exceeds the sum of all subsequent weights.
Consequently the digit coding is injective (Theorem 1.8): a represented target
has only one support, recovered by the greedy rule. For the integer
weights, both the scale and the cutoff matter. If
Indeed, with
Rounding the head down loses less than one, while rounding the later
terms down can only increase the difference. The resulting integer is
greater than
When a finite construction is proved to encode a fixed greedy target,
its choices are constrained by that support. Injectivity alone does not
identify an arbitrary finite approximation with a real greedy prefix.
Nor does it exclude averaging over indices, moduli, nearby targets or
auxiliary constructions.
Sources: weightedBoolSum_separated,
three_mul_tailWeight_add_exactLateGap_eq_three_mul_headWeight,
positiveMersenneDigitValue_injective.
The six limitations below require separate arguments. Fixed-target uniqueness explains canonicalisation (2.2); the recorded identities determine which sufficient conditions are equivalent to their goal (2.3). Measure and category (2.6), observation scales (2.4), finite versus infinite membership (2.5), and the hypotheses of the support certificate (2.7) do not follow from injectivity alone.
Uniqueness of the specified greedy words
Proposition 2.2 (Uniqueness under the stated finite
conditions). Put
If
and , then .If
, and , then .Let positive integer weights
satisfy for a positive integer . For a nonnegative integer target , let be the word obtained by visiting these weights in order and taking each when it fits. An admissible Boolean word has if and only if and .
Part (iii) gives uniqueness under the small-remainder condition, not existence. Theorem 6.100 gives a one-weight counterexample to dropping that condition.
Proof. For (i), truncate
Excludes at fixed depth. Under the three canonicalisation hypotheses just stated, a proof cannot gain freedom by choosing a different admissible word for the same target and depth. This says nothing about families satisfying different approximation conditions, or about averaging over depths or auxiliary data.
What the finite tests show. Three different
calculations are recorded here. For unrestricted prefix residues, the
proposed
At
Long prescribed digit strings also occur for unrestricted finite
words: the recorded examples at
The integer-window search reported no counterexamples for
Remark 2.3 (A sufficient condition that is not necessary).
The natural sufficient condition via fractional split-mass is
not necessary on real crossing cores: the example splitFractionMass_one_bound_not_necessary_fixture).
The example refutes necessity of that sufficient condition. It does not
refute using the condition on a class of cores for which it can be
proved.
Equivalent formulations of half-membership
The six conditions below are equivalent to half-membership. Their
common reason is the carry identity: a fixed nonzero difference from
Lemma 2.4 (Carry and residual value). Let
where
Proposition 2.5 (A cofinal carry bound). If
Proof. Lemma 2.4 gives
The right side is
erdosSupportSeries_greedyMersenneSupport_le).
Since mem_mersenneAchievementSet_iff_greedy_survival. ◻
Lemma 2.6 (The terminal bound at square depths).
Suppose
Proof. By Lemma 2.4 with halfStripBound)
with no slack required. ◻
At the depths integerHalfCarry_inter_Iic_eq_of_succ_le.
An achieving half-support excludes rank one because
Proposition 2.7 (Six equivalent membership
conditions). Each of the following is logically equivalent
to
for every ;there are arbitrarily large positive exponents outside
;at arbitrarily large depths
, some satisfies ; no agreement between the sets at different depths is required;at arbitrarily large
, ;at arbitrarily large positive depths
, some satisfies ;the half-target greedy remainder never exceeds the full remaining tail, so no finite fatal gap exists; the seven equivalent forms in the later classification express this same condition.
For (d) and (e), the reverse directions use the square depths in
Lemma 2.6. For
(a), membership gives
Scope of the equivalences. These conditions are
equivalent to membership, not strictly weaker substitutes. Equivalence
does not make a formulation useless as an invariant, but it does mean
that proving any of them is the same problem as (H). The equivalent
conditions remain unproved. In particular, mutually
incompatible witnesses at different endpoints do not buy a
weaker sufficient condition, and the
Scope limit. Item (a) does not extend to
every
The size of the required error bounds
One sufficient half-membership argument requires the reset inequality
For the
normalised deviation
Class (a): fixed precision or bounded state. The following three statements concern abstract recurrence models. Their conclusions apply to the Mersenne problem only within the specified models; they do not use its full divisor-count constraints.
Proposition 2.8 (Limits of the specified local
summaries). (i) After
Their binary sums
are all
For an integer recurrence
Class (b): global averages and Diophantine data.
Proposition 2.9 (A bound for the reduced
denominator). Let
The middle
inequality is strict when the skip set is nonempty; for an empty skip
set both sums are zero. This is an upper bound, not a quadratic
asymptotic for
Scope of these obstructions. The common pre-index history in Proposition 2.8(ii) does not determine the post-index tail in its countermodel family. This does not exclude a state using additional arithmetic input from the actual support. The displayed denominator bound combined with the cited fixed irrationality-measure exponent does not yield the required run bound. These calculations do not exclude averaging over shifts, residues, or observation scales, nor a sharper analysis of the actual skip distribution.
Prime steps and bounded windows. In the universal
recurrence, a prime step subtracts
Remark 2.10 (Status of the exhaustion claim). The preceding counterexamples concern the specified finite summaries and estimates. They do not classify all available tools, even within the broader categories of local information and global averages. No exhaustion claim is used in a subsequent deduction.
What finite certificates decide
Theorem 2.11 (One-sidedness). Non-membership of
Proof. The dichotomy half_mem_mersenneAchievementSet_or_exists_fatal_gap),
and the two alternatives are exactly complementary (existsFatalHalfGap_iff_half_not_mem_mersenneAchievementSet),
with ExistsFatalHalfGap
a finite witness type. In the other direction, certified death implies
non-membership (certifiedGreedyMersenneDeath_not_mem,
over CertifiedGreedyMersenneDeath;
three_fourths_certifiedGreedyMersenneDeath),
whereas the absence of a certificate through depth
Finite search versus infinite survival. A discovered fatal-gap certificate proves non-membership. Further surviving prefixes give larger verified ranges, but do not establish membership without an argument covering all ranks. This distinction is unchanged whether one increases the geometric truncation depth, the number of quotient rows, or the depth of a grouped computation. The different finite parameters should not be reported as a single verification depth.
Why measure and category do not decide a rational target
Remark 2.12 (Achievement-set geometry does not decide rational-target membership). The achievement set has positive measure and is nowhere dense (Theorem 1.8). Neither fact alone decides membership of a specified rational. Injectivity fixes the support of an achievable value, but it does not exclude averaging over indices, shifts, residues, observation scales or auxiliary constructions. The recorded calculations obstruct the particular models and estimates analysed here; no impossibility theorem for all probabilistic, measure-theoretic or averaging methods is claimed.
The geometry itself is Lean-checked in Theorem 1.8:
Hypotheses of the CRT block-certificate argument
Observation 2.13 (Two inputs to the CRT certificate argument).
The CRT block-certificate arguments considered here require both
compatible divisibility prescriptions and a tail estimate strong enough
for the height inequality
What remains to check. One cannot apply a
conditional CRT certificate theorem to arbitrary infinite
Explains only a method boundary. The primes are
infinite and pairwise coprime, so they satisfy the first input. The
identity compositeDilationDefect_eq_zero_of_prime_support
makes the dilation algebra exact there; yet this certificate theorem
does not apply because
The distinct estimates still required
The half-target analysis involves a geometrically weighted divisor
sum
Unproved inputs for further arguments
The preceding counterexamples leave estimates that could still be used in the conditional arguments. Some would imply membership; others are equivalent to it. The prime-support question asks for a formal recovery of a known theorem. For each proposed estimate we compare its hypotheses with the relevant counterexample. The list is not exhaustive.
Two further analytic tests
Small displacements at a real base do not by themselves give the
fixed rational lattice used in the integer-base proof. For
along some sequence of positive integers
To justify the conditional implication, suppose instead that
The infinite support makes
Using
The asserted limit would contradict
this inequality. The multiplier
A different extension requires squarefree remote-tail control and a weighted displacement to be small at the same indices. CRT establishes compatibility of the finite opening divisibility conditions, but not this simultaneous smallness. Neither argument is claimed to establish its required analytic hypothesis.
A lower bound at reset ranks
What it needs. Either of the first two sufficient conditions below. Their different scales do not establish an implication between them. The sign condition (iii) is a separate question; no implication from it to half-membership is proved here.
Reset-deviation bound. For every upper or middle reset row
, require . Section 12.5 states the exact conditional implication to membership. A run-length estimate is a possible way to approach this bound, not an established exact reformulation of it.Band avoidance at resets, already proved to imply membership. For every upper reset
(branch of Theorem 5.16) and every , the reset charge avoids the linear-width band .Sign law alone. At every reset, M-resets have
and U-resets have . This specifies the sign but not a quantitative distance from zero. Neither an implication to half-membership nor a strict comparison with the first two conditions is established here.
Sources. SeamUpperResetDyadicBandEscape
with conditional implication half_mem_mersenneAchievementSet_of_upperResetDyadicBandEscape;
quantifier collapse dyadicBandEscape_iff_exists_critical,
which reduces the seamUpperResetDyadicBandEscape_through_thirty;
alternative implication LargestSkipLateStepSocket
with conditional implication half_mem_mersenneAchievementSet_of_largestSkipLateStepSocket
and base case largestSkipLateAt_fourteen.
Logical strength. The reset bound is a sufficient condition for half-membership in the cited argument. No converse is established here. The fact that it is quantitative, while membership is qualitative, does not prove that the condition is strictly stronger: that would require a separate implication or counterexample. The carry identity of Proposition 2.5 does not itself furnish this lower bound on the reset deviation.
What the finite checks establish. The reported
computation checks the reset inequality over its stated range, with
margins of
Uniqueness in Section 2.2 does not prevent this argument: the proposed bound concerns the actual greedy sequence. It does not require alternative supports for the same target.
Run lengths. The record reports a maximum
right-branch run of length
The missing step is the quantitative lower bound itself. The finite observations do not supply the growing-precision estimate discussed in Section 2.4; it remains unproved.
Increasing the depths of exact finite sums
What it needs. Rule out the recycle branch returning to a bounded endpoint forever. Any one of:
critical quotient supply: for every below-half core
bounded by with genuine crossing deficit, ;a direct proof that the crossing rank
produced by the recycle branch cannot repeat the value , or any bounded value, infinitely often;a growth law for
as a function of the incoming endpoint .
By Proposition 2.2(ii), form (a) need only
be checked along the one canonical orbit, the half-target
greedy prefix, not searched over
Sources. exactLocalMersenneHalfRow_double_or_recycle;
the formal counterexample exists_seeded_bounded_double_or_recycle_model
(the model skippedCoreSharpCapacity_below_or_strictly_laterExactRow;
unconditional recycling exists_skippedCoreExactRow_of_value_above;
hypothesis SkippedCoreCriticalQuotientSupply;
capacity equivalence localBinarySuffix_two_mul_sub_two_lt_criticalCapacity_iff;
seed example exactLocalMersenneHalfRow_six.
The finite-row test and its unique candidate. The
real-prefix argument in Proposition 2.2(ii) does not by itself
identify an exact-row witness. The integer weights have a separate,
decisive property: for fixed
form a decreasing sequence in which each
weight exceeds the sum of all later weights by at least
This integer greedy word should not be silently identified with the
real greedy prefix
Finite decidability and the cofinal requirement. The test decides the exact-row predicate at any specified depth. The claim that successful depths are arbitrarily large is still equivalent to half-membership, by Proposition 2.7(c). Neither uniqueness nor finite decidability supplies that cofinal assertion. The double-or-recycle argument must prove genuine progress in the depths, not rely on a purported freedom to choose many witnesses at one depth.
The known prime-support theorem
The base-
by expanding each reciprocal Mersenne term geometrically and collecting divisors. Tao and Teräväinen prove the right-hand series irrational in Theorem 1.3 of Quantitative correlations and some problems on prime factors of consecutive integers. Their proof is analytic and is cited here; it is not formalised in Lean.
The local pairwise-coprime certificate theorem still does not cover
the primes because it assumes summability of
Equivalent membership conditions
Proposition 2.7 lists the
equivalent conditions: a pointwise upper bound on integerHalfCarry_eq_scaled_residual_add_tail,
binaryCoeffTail_nonneg,
binaryCoeffTail_supportCoeff_le_two_sqrt_add_four,
and, for the terminal-strip conditions, evaluation of the square root at
a perfect square. The one-sided scope limitation in Proposition 2.7 still applies
to general supports.
Purpose of the equivalences. These results identify the exact logical content of the proposed hypotheses. They do not settle half-membership, nor do they make an equivalent formulation useless: a different expression of the same condition may expose an invariant or a more convenient induction. The formalisation task is separate from the unproved arithmetic assertion on either side.
Why zero windows do not split the support class
One proposed split asks whether every infinite support satisfies
For the present divisor counts, the first
alternative never occurs. Writing supportCoeffZeroWindow_length_le_eps_logb
therefore does not split the support class into two useful cases. The
lcm-gap theorem irrational_erdosSum_of_lcm_gap
remains an independent irrationality result, not an instance of this
zero-window alternative. The proposed assertion consequently requires
block certificates for every infinite support: for each required
precision, one must construct an opening block with
This reformulation does not remove the CRT compatibility and tail-estimate requirements of Section 2.7. It asks for a new construction that meets them for general supports. Nor does it identify that construction with the reset estimate used for the half-target: the two arguments use related divisor-count identities, but no equivalence of their missing hypotheses is proved here.
Comparison of the remaining inputs
Route 4 packages recorded equivalences; it does not establish their unproved existence hypotheses. Route 3 must be compared with the external prime-support theorem of Tao and Teräväinen [8]; reproducing it in this framework requires its own analytic input. Route 2 offers a different finite search space under the conditions stated there. Routes 1 and 5 share some incidence identities, but this is not a proof that every missing hypothesis is equivalent. The appropriate comparison is the input each route needs, its quantifiers, and what a successful estimate would imply.
Reading the detailed record
Part III groups the finite arithmetic by object: divisor certificates, greedy coding, quotient identities, carries and support restrictions. The implication tables show how to pass between these descriptions and where an additional hypothesis is needed. The preceding two sections supply the corresponding comparisons with failed estimates and remaining analytic questions.
The reported calculations concern
III. Detailed statement and arithmetic catalogue
The series, the greedy rule and finite identities
Expanding a Mersenne weight as a binary geometric series converts a support into its divisor counts. We use that identity to compare real greedy remainders with finite integer quotients. Rounding introduces an error depending on both the scale and the cutoff; keeping those parameters separate is necessary for the later orbit estimates.
The object
In this part, write
Definition 5.1 (Universal Problem #257). Is
The support theorems prove irrationality for specified infinite
families. The following question instead asks whether one particular
rational number is represented. A positive answer would disprove the
universal assertion; a negative answer would settle only that target.
The later analysis also treats
Definition 5.2 (The distinguished half-value
question). Define the Mersenne achievement set
Observation 5.3 (Why the half-value question controls
universal #257). Any finite subset sum of positiveMersenneSupportValue_coe_finset_ne_half).
Consequently, if
What is proved
Full-support irrationality, for every base
Theorem 5.4 (Full-support irrationality,
unconditional, every base
Hypotheses:
This formalises the positive-integer-base scope of Erdős’s classical 1948 full-support theorem, which already covered integer bases of absolute value greater than one. The base-two Erdős–Borwein constant is a particular case; the Lean theorem is recorded with no open hypotheses.
Structured infinite supports
Beyond full support (
Theorem 5.5 (Purely periodic support). For
integers
Theorem 5.6 (Eventually periodic support). For
integers
Theorem 5.7 (Residue-class support). For
integers
Theorem 5.8 (Odd support). For every integer
A support representing
Topology and measure of the achievement set
Theorem 5.9 (Achievement-set topology and measure).
Use: Theorem 5.10 below
(compactness is exactly what powers every “limit of achieved points is
achieved” argument used downstream, including the seam-limit route of
Part 2).
Theorem 5.10 (Membership equals greedy survival at
every level). For a real
The inequality says that the unselected tail has enough total mass at every rank. A failure at any one rank excludes membership; the inequalities at all ranks give a representation.
The greedy rule for one half
Fix the target
Definition 5.11 (The half-value greedy orbit). Let
Take iff
; if taken, .Skip otherwise;
.
A skip at rank
safe iff
(the total remaining mass does not yet rule out a representation; this inequality alone does not guarantee one);fatal iff
(the residual is too large for the remaining tail to ever reach, yet too small to have been taken at – an impossible gap).
For example, ranks
By Theorem 5.10,
Remark 5.12 (No-ties: both greedy-orbit boundaries are
strict). (a)
Integer quotients and their remainder identity
The quotient rows are finite integer approximations to the real
greedy rule, not identical finite stages of that rule. Their normalised
weights tend to the Mersenne weights and their targets tend to
and the integer target
is
Definition 5.13 (The full-support quotient
recurrence). For
This depends only
on
Here
Theorem 5.14 (Decomposition of the integer remainder).
For every quotient row
Here the take and skip sets, capacity and
remainder are those defined at the start of this subsection. The
identity separates the contribution of the full exponent range from that
of the omitted ranks. It makes no claim that there are few omitted
ranks; controlling their sum is a separate part of any
application.
Proof. For
Substitute this in the
definition of
Use: (I) permits substitution of information about
A real-valued form of the quotient identity
Theorem 5.15 (Real (non-integer) form of the quotient
identity). Let
where
Proof. Splitting the full
series at
The
tail bounds
Use of the error bound. For
Note:
Dynamics
Theorem 5.16 (Exact recurrences for the three
branches). Fix
and define the two correction terms by
Both
lie in
Consequently, for
Proof. Applying the one-step quotient identity twice gives
The new
capacity is
Only the
There is no
Thus
Iterating the
Reported finite checks
The following values and finite ranges come from exact integer
computations for the quotient-greedy sequence of Section 5.4. They provide test
cases for the formulas above. The low-row remainders at
Observation 5.17 (Exact low-row values). At row
Source: the values at rows seamUpperResetDyadicBandEscape_through_thirty.
The two ranges differ by one: the remainder used for reset
Observation 5.18 (Depths of the reported computations). The
quotient identity (Theorem 5.14) is verified at
rows
Observation 5.19 (Four computations side by side). Four
related computations are reported, with different targets or integer
representations, at the following ranges: truncation rung
Use: truncated weights define a different greedy problem, and
the quotient-row construction uses integer weights rather than the
original real weights. These are not automatically four readings of the
same decision stream. Their relevance to full-weight membership comes
from the approximation, limit, or identification theorems cited for each
construction. A certificate at one range does not transfer to another
without such a theorem, and these reports do not decide the universal
problem.
Detailed results and their hypotheses
The catalogue begins with conditional membership tests, then gives the identities and invariants used in their proofs. Its final groups record consequences and counterexamples. Each result retains its hypotheses, and the margin identifies its associated formal proposition. The support results and these conditional tests leave the universal irrationality assertion unresolved.
Conditional membership tests
The finite tests below use
Theorem 6.1 (Infinitely many greedy skips force
membership). Fix
Proof. The identity
Theorem 6.2 (The quotient remainders converge to the
greedy deficit). Let
In particular, the following
conditions are equivalent:
Proof. For each fixed
First letting
For
The two error terms tend to zero, proving the asserted limit. The real
greedy sums never exceed
Convergence itself is automatic; proving that its limit is zero is exactly the unresolved membership question.
Theorem 6.3 (Two-channel and dyadic cap sufficiency).
Suppose that for every
Then
Theorem 6.4 (Second-channel phase separation
sufficiency). Define
then
Unlike Theorem 6.3, this
hypothesis concerns every positive rank, not only skipped ranks. It
excludes an explicit interval around
Theorem 6.5 (Straddle-prefix closed-set criterion).
Suppose that for every
Then
Theorem 6.6 (Keeping the largest skipped rank beyond
two thirds). Let
Then
The cited finite calculation establishes the initial inequality
at row
Theorem 6.7 (Two sufficient bounds at middle
transitions). Suppose that at every middle transition with row
Then
Indeed,
Theorem 6.8 (The tail inequality at a final middle
transition). Suppose row
Then
Theorem 6.9 (A conditional two-sided dyadic bound).
Assume the following two conditions for every row
Then at every row
The first hypothesis concerns only middle
transitions. The second concerns only right transitions at which the old
overshoot is at most
Proof. At row
On a right branch, an old remainder at most
This conclusion is a disjunction. It does not by itself give an upper bound for the remainder on rows where only the overshoot is small, and therefore is not by itself a membership criterion.
Theorem 6.10 (Upper-reset dyadic-band escape, checked
for
Theorem 6.11 (Möbius-centred carry nonnegativity below
The carry is an integer,
so it is at least
Theorem 6.12 (A square-root bound on the greedy
carry). For the greedy support
then
Theorem 6.13 (Equivalent sign and vanishing
conditions). For the prefix
This is a finite integer expression: it compares the
next
For every skipped rank
, .For every skipped rank
at which the real and integer greedy words agree on , .For every skipped rank
, .
Conditions (i) and (ii) are equivalent. Condition (iii) implies them; no converse or strict separation is established here. These hypotheses must hold at every indicated skipped rank, not merely through a finite computed range.
Theorem 6.14 (Erdős–Borwein full-support
irrationality, unconditional). For every integer
Theorem 6.15 (Pairwise-coprime support irrationality,
Erdős 1968). For every integer
Theorem 6.16 (Irrationality from divisible coefficient
blocks). Let
Then
Proof. Write
Positivity follows from the
specified nonzero coefficient beyond
If
A certificate at one precision is not enough: the same coefficient
sequence must satisfy these conditions for every
Theorem 6.17 (Irrationality from a gap beyond the
preceding least common multiple). For an integer base
Theorem 6.18 (Factorial-support and
are irrational. These are
instances of the preceding theorem. For the factorial support the
preceding least common multiple is
Theorem 6.19 (Multiples-support irrationality via
dilation). For integers
is irrational. This is the full-support result (Theorem 6.14) at the
integer base
Luca and Tachiya proved irrationality for every purely periodic integer weight that is not identically zero [3]. The periodic, eventually periodic, residue-class and odd-support statements below follow from their theorem; their Lean proofs are separate and use the certificate method described here.
Theorem 6.20 (Periodic-support irrationality).
Let
The indicator of
Theorem 6.21 (Eventually-periodic support
irrationality). Let
Theorem 6.22 (Residue-class and odd-support
irrationality). For integers
Comparison with the known theorem.
Luca and Tachiya proved irrationality for every nonzero purely periodic integer weight, of any signs [3], so the terminating branch below occurs only for the zero weight. The theorem records the dichotomy reached by the certificate method, together with its one-sided closures.
Theorem 6.23 (A formal dichotomy for signed periodic
weights). Let
The cited formal argument gives the
dichotomy that
For the next two results write
Every
quotient in
Theorem 6.24 (Denominators of finite Mersenne sums).
Let
In particular,
Theorem 6.25 (Exponential growth of the reduced
denominators). For an integer
where the product
is over primes. Then
Proof. Apply Bertrand’s postulate [24] to
The exact expression for
The Lean proof of the bound uses natural-number division
Exact identities and reductions
Observation 6.26 (A finite half-value approximation and the first correction tail). The finite prefix has value
The excess of the full tail after rank
Indeed, expand each
summand as
Observation 6.27 (Period-4 sign weight vanishes on a residue
class). Let
Indeed,
intWeightedCoeff_periodFourSignWeight_eq_zero_of_mod_four_eq_three
Theorem 6.28 (The Lambert-series identity for the Möbius function). The absolutely convergent signed series satisfies
This classical identity is also recorded in [7]. Expand each denominator
geometrically and interchange the absolutely convergent sums. The
coefficient of
Corollary 6.29 (Negative-Möbius Boolean support
overshoots
since
Observation 6.30 (Dyadic safety need not survive a take). For
a residual
The residual
The same failure occurs with an initial denominator containing all
Mersenne denominators through rank
The initial residual is at most
safeBracket_and_numeratorMonotone_not_inductive_fixture
lcmSaturated_safeBracket_not_inductive_fixture
Theorem 6.31 (The half-skip dichotomy via Erdős–Borwein irrationality). The half target satisfies
where
Theorem 6.32 (Equivalent descriptions of
half-membership). Each of the following is equivalent to
The integer-greedy sequence is not eventually always on branch
.There are arbitrarily large
with .Upper or middle transitions occur at arbitrarily large rows.
Some sequence
satisfies for every .There are rows
and omitted ranks with .The positive ranks omitted by the real half-greedy rule form an infinite set.
The real half-greedy rule has no last omitted positive rank.
Items (1)–(4) differ only by the branch classification and the choice of a sequence of rows. Item (5) requires the omitted ranks themselves to tend to infinity, not merely their containing rows. The cited identification with the real greedy support supplies (6)–(7). These equivalences do not prove that any of the conditions holds.
Lemma 6.33 (The values on either side of an eventual
right continuation). If the seam eventually always extends “true”
(right branch) from some row
Lemma 6.34 (Each Mersenne weight exceeds its remaining
tail). For
For the upper bound, compare
each tail term with
It is not available for the totient weights
Theorem 6.35 (Greedy survival and membership).
With the greedy remainder
If all
inequalities hold, the nonnegative remainders tend to zero because
Lemma 6.36 (The two next-prefix intervals and their
gap). Let
or in the upper interval
or in the open gap between them. These alternatives are disjoint because
Lemma 6.37 (A greedy gap excludes every
representation). Let
then no support agreeing with
Lemma 6.38 (No finite Mersenne sum equals one half).
For every finite
Lemma 6.39 (Straddle words are canonical: they agree
with the greedy prefix). Let
where
Theorem 6.40 (Last-skip iff local fatality: a
pointwise criterion). Keep
Thus it suffices to check the tail inequality at the ranks actually omitted by the greedy rule. This is an equivalence on that fixed orbit; it does not establish the inequality at its unboundedly many possible omitted ranks.
Lemma 6.41 (Seam upper-or-middle classification).
At a row
or this inequality fails and
These are exactly branches
Lemma 6.42 (The exact gap at the largest omitted
rank). Let
The correction is independent of the common prefix
Proof. For
Subtract the sum over
For example,
Theorem 6.43 (Reduction to the nearest dyadic
boundary). Let
For
Theorem 6.44 (Excluding minus three at a final middle
transition). Suppose that row
This excludes one particular value under the stated tail assumption; it neither excludes every final middle transition nor proves the all-middle-row hypothesis of Theorem 6.9.
To see the contradiction, complete
Lemma 6.45 (The signed position of a skipped greedy
prefix). Let
Exactly one of the following holds:
Thus the real greedy prefix is one of the two
adjacent integer words. This classifies its signed distance
Lemma 6.46 (Spacing of reverse-carry words). For
Let
The factor in
parentheses is an odd integer. If the two terminal carries have absolute
values at most
Lemma 6.47 (Linear functionals factoring through one
value). Let
Theorem 6.48 (Two-thirds band: exact localisation of
post-take skip-unsafety). Write a positive residual as
Clearing the
positive denominators proves the equivalence. The interval has width
For a single skipped rank,
These are local transition statements, not bounds on the actual
half-greedy orbit. Dyadic safety is only sufficient for the current tail
test. The odd-coprime data
Theorem 6.49 (A weaker sufficient test against the
remaining tail). Let
ensures
The containment of these sufficient conditions is strict even for
valid rational data:
Lemma 6.50 (Summability of one gap length per level).
For
This follows by summing the per-level upper bounds geometrically. It is
not the measure of the union of all gaps: level
Lemma 6.51 (The effect of adding one divisor).
Let
In particular, the difference is
Theorem 6.52 (Uniqueness of an integer recurrence with
a vanishing scaled limit). For any nonnegative-integer coefficient
sequence
Lemma 6.53 (Changing finitely many support elements).
Let
Lemma 6.54 (An integer test for the interval between
the dyadic and Mersenne weights). For positive integers
The first test concerns the dyadic bound, not the greedy selection threshold itself. The second identifies precisely the interval in which a Mersenne weight is skipped but the dyadic safety test fails.
Lemma 6.55 (The odd denominator survives dyadic
subtraction). Let
Lemma 6.56 (A guaranteed divisor of a reduced
denominator). Let
Thus scaling may remove part of the guaranteed divisor. Indeed,
reduction divides
Lemma 6.57 (Commuting prime-power differences).
For a function
These operators commute. If
Thus the mixed
difference counts precisely the support elements whose
Proof. Expanding either order gives the same four terms:
This commutation needs no primality or
coprimality. For
For
Definition 6.58 (The Mersenne achievement set and the
support-series object). For a support
Finite, empty,
and infinite supports are all allowed in
Proposition 6.59 (Achievement-set topology: compact,
closed, perfect, measure exactly one).
Theorem 6.60 (Nonmembership of one half and a finite
fatal gap). The value
One implication is Lemma 6.37. For the other, follow the greedy prefixes: nonmembership forces a first failure of the tail inequality, hence one of these gaps. The endpoint equalities are excluded by Lemma 6.38.
A finite prefix and strict gap provide a nonmembership witness.
The tail inequality can be certified by rational truncation bounds as in
Theorem 2.11.
Membership, in contrast, asserts that no such witness exists; failure to
find one in a finite search is not a proof. The reduction uses
Definition 6.61 (Separated integer values and bounded
perturbations). Let
The updated values are
The inequality
Theorem 6.62 (Perturbed-family maximality and the
three-branch recurrence). Use the family and adjacent pair of
Definition 6.61, and assume
in addition that
Proof. The lower candidate satisfies
On the first branch the remainder is at most
The theorem describes a two-stage rule, not automatically the maximum
of
The hypothesis
Consequence theorems
This subsection concerns finite sets
Finite quotients and their remainders
Definition 6.63 (An exact finite quotient sum). For
an integer
The word “exact” refers to this integer
equality, not to
Definition 6.64 (Floor quotients and the signed endpoint expression).
The signed endpoint expression has three arguments:
The suffix in this formula is defined next. The quotients are integers; this final expression is allowed to be negative.
localPrefixQuotient
localMersenneQuotient
localRepairInteger
Definition 6.65 (The remaining binary suffix).
the nonnegative remainder after subtracting the
quotient contributions from the nonterminating binary expansion of
Definition 6.66 (Exact quotient sums at unbounded
depths). The cofinal exact-row condition says that for every integer
No agreement is required between supports chosen at different depths. This removes a compatibility requirement from the data to be supplied, not from the underlying membership question: Proposition 2.7 identifies this cofinal existence statement with half-membership. A failed construction of compatible rows therefore does not refute the condition, and the condition itself is not proved here.
Two implications yielding half-membership
Theorem 6.67 (Compactness from exact finite sums).
Suppose the cofinal exact-row condition in Definition 6.66 holds. Then
Every
Theorem 6.68 (Infinitely many greedy skips suffice).
Suppose that the greedy remainder for
Then exact quotient rows exist at
unbounded depths, and
Compatible finite approximations
Theorem 6.69 (A compatible family of finite
supports). Let
The four conditions
on the finite rows, required for every
The first condition implies that the integer in
the next two lines is nonnegative. The second specifies the binary value
of the upper half of the row, the third bounds that value by its
available number of bits, and the fourth is the exact quotient equation.
The maximum in the first line records natural-number subtraction at the
case
These are the finite hypotheses of the compatible-limit
construction. The bit condition fixes coordinate
The existence of rows satisfying these four conditions for every
A quotient bound at a crossing
Theorem 6.70 (A sufficient quotient bound at a
crossing). Consider the following condition on finite sets
It requires the quotient inequality at every
strict crossing of one half by an added weight. Theorem 6.93 identifies this
inequality with the binary bound needed in the finite construction. If
the condition holds for all such
Theorem 6.71 (Induction from the depth-six example).
An already-formalised induction from the endpoint-six seed
(Definition 6.97) consumes
Theorem 6.70 at
every step: each protected exact row either doubles below half
(unconditional) or recycles at its first crossing rank
Theorem 6.72 (The quotient condition on greedy
prefixes). Let
It asks for the quotient bound at every skipped rank of the specified half-greedy orbit. This restricts the crossing test of Theorem 6.70 to its actual greedy prefixes. The finite uniqueness results justify that restriction where the cited induction uses it; they do not prove the displayed inequality.
Theorem 6.73 (Two consecutive skips). If
The one-step
quotient recurrence gives
Proof. The two skips imply
where the last inequality holds for
Theorem 6.74 (A later skip after a selected block).
Suppose the real half-greedy rule skips rank
then the precritical suffix bound at
To obtain cofinal exact rows by this result, the stated gap
condition must hold at cofinally many skipped ranks
Filling the remaining binary positions
Theorem 6.75 (Filling the remaining binary
positions). For any
there is an exact row
Theorem 6.76 (An exact sum at depth
This conclusion forgets the additional support-extension information in that theorem. It is the form used when only the existence of an exact row is needed.
Proposition 6.77 (Quotients in the upper half of the
index range). For integers
Indeed, the quotient is
Theorem 6.78 (A finite sum from a skipped prefix).
Let
Then there is
For a finite
Reducing the dyadic-boundary checks
Theorem 6.79 (Testing one nearest dyadic boundary).
Let
The boundary
Proof. For
For example,
At an actual upper reset, Proposition 6.80 supplies
Proposition 6.80 (An upper bound for the reset
expression). Let
The
nonnegativity of the successor remainder therefore gives
Nonnegativity of the omitted-tail margin
The next three statements compare the conditions of Theorem 6.13. The first two are equivalent; the third is sufficient for them.
Definition 6.81 (A nonnegativity condition at skipped ranks).
This condition is not
established here. Its usefulness is the following implication: assuming
it, a Lean theorem proves
HalfGreedySkippedFullShellNonnegative
half_mem_mersenneAchievementSet_of_skippedFullShellNonnegative
Theorem 6.82 (An equivalent vanishing condition).
This condition is equivalent to Definition 6.81. At an actual
skipped rank, the source proves that
Theorem 6.83 (A sufficient lower bound for the integer remainder).
a
sufficient condition for the nonnegativity condition above. Indeed, a
negative margin at an actual skip would force
The displayed lower bound itself is not established.
Square-root bounds for half-carries
Theorem 6.84 (A square-root carry bound implies
half-membership). Write
then the greedy selected support
Theorem 6.85 (Terminal bounds at unbounded depths).
Suppose that for every
Then some infinite
These are not the exact-row conditions of Definition 6.66. For such a finite support,
so an exact row has carry
The hypothesis is not established.
Theorem 6.86 (Cofinal returns of the greedy carry).
Suppose that for every
Then
A margin at an unspecified later horizon
Theorem 6.87 (An eventual nonnegative margin
suffices). Fix a positive depth
Here
This normalised expression, not necessarily
The result supplies some finite horizon, not the horizon
Equivalent conditions for infinitely many greedy skips
Theorem 6.88 (Half-membership and infinitely many skips).
Odd-denominator parity supplies the positivity clause in Theorem 6.68 automatically. Thus its cofinal-positive-skip hypothesis is exactly the assertion that the greedy skipped support is infinite, which the displayed theorem identifies with half-membership. See Observation 6.132 for the reason this restatement does not itself prove membership.
Invariants
This subsection collects identities and bounds used in the preceding criteria. Each statement retains its own hypotheses; a bound for one branch is not an invariant of the entire recurrence.
One-step quotient identities
Theorem 6.89 (The next floor quotient). For
Indeed,
Theorem 6.90 (The next quotient sum). For a
fixed finite set
This is the
sum of Theorem 6.89 over
Theorem 6.91 (The signed endpoint recurrence).
The signed next-step expression is
Bounds for the remaining binary positions
Definition 6.92 (The sharper binary bound). Let
It permits a binary completion using ranks
Theorem 6.93 (Equivalent forms of the sharper bound). Under the hypotheses of Definition 6.92:
The threshold on the right is one greater than the
exact-row target
Proof. Put
For the completion, use the ranks
For example,
Theorem 6.94 (An unconditional bound with one extra
bit). Unconditionally, for every
The bound holds uniformly in
Doubling the endpoint
Theorem 6.95 (The binary bound after doubling).
Let
The missing
quotient can therefore be filled using only the ranks
Proof. Write
The
below-half assumption makes this an ordinary integer difference, so no
truncation is needed. Since
using
For example,
Proposition 6.96 (Every exact sum contains exponent
two). Let
The depth-six example
Definition 6.97 (An exact sum at depth six). The set
hence it is an exact row at
depth
Approximation error and finite denominators
Proposition 6.98 (Error in the finite subseries
value). An exact row at endpoint
Proposition 6.99 (No finite support has value one
half). A finite sum of reciprocals of odd integers has odd
denominator in lowest terms, so it cannot equal
Uniqueness for gap-dominated finite weights
Theorem 6.100 (Small remainder forces the greedy
word). Let
Fix an integer capacity
Indeed, two different words have sums
separated by at least
Proposition 6.101 (Gap domination of the integer
weights). For integers
Thus the finite weight list at ranks
Proposition 6.102 (Uniqueness of the finite greedy
representation). Let
then
A geometric form of the quotient condition
Theorem 6.103 (A division-free form of the binary
bound). For
where an empty sum
is zero. To see this, write
Bounds for a general coefficient sequence
Rationality of a binary coefficient series gives an integer recurrence. The necessary decay condition is on the scaled recurrence, and allows unbounded integer values. We first bound the coefficient tail, then recover the series value by telescoping. For support series, Möbius inversion imposes an additional condition on the coefficients.
Theorem 6.104 (An upper bound for a binary coefficient
tail). Let
Indeed,
Theorem 6.105 (Rationality through an integer
recurrence). Let
The limit condition is
To prove the forward implication from a recurrence, we telescope:
The limit condition gives the rational value
For example, the finite support
Theorem 6.106 (Möbius inversion of the divisor
counts). For a set
where
Theorem 6.107 (The support series as a coefficient
series). For
Expanding each
denominator as a geometric series and interchanging nonnegative sums
gives the identity. Since
Restrictions on a support with rational value
The next results impose separate restrictions on rational-valued supports. The related strict-gap result is Proposition 6.99.
Theorem 6.108 (A restriction on dyadic rational
values). If an infinite support
Theorem 6.109 (Unboundedness of a positive shifted
recurrence). Let
Then
Theorem 6.110 (Bounds for intervals with zero divisor
counts). Suppose that
Proposition 6.111 (A subpower bound for divisor
counts). For positive integers
Proposition 6.112 (Two distinct prime-power
differences commute). Lemma 6.57 gives
the four-term expansion and its divisor-count interpretation.
Commutation is elementary for arbitrary positive multipliers. The
extraction formula uses distinct primes, positive exponents
The first crossing of the half-value
Definition 6.113 (The first crossing rank). For a
finite set
the ranks at which
Theorem 6.114 (Existence of a first crossing).
Let
Positivity of the
summands makes the partial sums increasing. Their odd reduced
denominators exclude equality with
Centred carries at skipped ranks
Theorem 6.115 (Nonnegative centred carries below the
half-value). If
Indeed, Lemma 2.4 gives
The first term is
strictly positive and the tail is nonnegative. Since the half-carry is
an integer, it is at least
Theorem 6.116 (Three possibilities at a skipped
endpoint). For a rank
Gap lengths and the measure of their union
Definition 6.117 (The gap after a Mersenne weight).
For
Theorem 6.118 (The unweighted sum of remaining gap
lengths). For every
which tends to zero. The estimate follows by summing the per-level
bound; it counts one length per level. It does not, by itself, bound the
measure of the union of all gaps, because there are
The measure of the union of gaps created after level
Indeed, the finite sum from
A sufficient test for a safe skip
Definition 6.119 (Three geometric terms in the tail
lower bound). For
mersenneTailLB3
three_div_lt_mersenneTailLB3
mersenneTailLB3_lt_mersenneTail
Theorem 6.120 (A sufficient inequality for a safe
skip). Let
The latter implication uses the three-term lower bound above. More
explicitly, with
The inequality
The sufficient condition is weaker than
Proposition 6.121 (Two unconditional safety cases).
Under the positive-integer and skipped-step hypotheses of
Theorem 6.120,
Two-sided bounds near dyadic endpoints
Theorem 6.122 (Two-sided dyadic bounds). Under the local hypothesis excluding the specified three middle cells and imposing the right-pulse bound, induction (base case at row 5 verified by direct computation) propagates it to the universal two-sided bound
This conditional bound says
that at least one of the remainder and the adjacent overshoot is at most
Proposition 6.123 (A finite band check for
It computes the
successor remainder at each row
General identities for perturbed greedy recurrences
Theorem 6.124 (A general perturbed greedy recurrence).
Let the old integer values be separated by at least
The underlying structure in Definition 6.61 assumes only
Theorem 6.125 (Spacing of compatible reverse-carry
words). Consider two integer carry recurrences
Proposition 6.126 (Changing one support bit at a
doubled rank). Let two supports agree except that the second
includes
Obstructions and countermodels
The results below test particular proposed implications. A countermodel to an abstract transition rule shows that the rule needs an additional hypothesis; it does not disprove a more structured arithmetic argument. Each entry states the information retained by its model and the conclusion that this information fails to imply.
Theorem 6.127 (A bounded model of the
doubling-or-return alternative). The dichotomy
The double-or-recycle transition shape, even together with an endpoint-six seed, is logically insufficient to conclude cofinal exact rows. A genuinely new progress input (strict endpoint growth, or an independent cofinality argument) is required. The countermodel retains only the seed and this transition rule. It therefore tests those premises, not additional arithmetic information that a more structured induction may use.
Theorem 6.128 (Doubling or returning to an earlier
depth). For
Every exact row of
depth at least
Proposition 6.129 (A sufficient fractional-mass bound
need not hold). Take
However, the combined fractional mass is
The linked Lean proof checks this
example by direct computation. Thus the combined fractional-mass bound
by
Observation 6.130 (A doubled finite sum can exceed one half).
Theorem 6.95’s
doubling extension is not preserved iteratively: below-halfness is not
preserved under one application of doubling, and demonstrably fails at
the very first step. From the identity
so the doubled row is strictly above half. Iterating
the cheap (doubling) arm is therefore impossible from the only recorded
seed; the chain is forced into the capacity-gated recycle arm at step
one. What would close the doubling route instead: cofinally many
below-half exact rows,
exists_exactRowStrictUpperExtension_two_mul_sub_one_of_exact_below
Theorem 6.131 (The returning endpoint need not be
larger). Theorem 6.78 is unconditional,
but its witness is
Observation 6.132 (The skip condition is equivalent to
membership). The positivity conjunct of Theorem 6.68’s hypothesis,
Theorem 6.133 (Uniqueness at a critical crossing).
For
Thus
Observation 6.134 (Different requirements on finite
witnesses). Theorem 6.85 (the cofinal
terminal-strip condition) tolerates any support inside the depth-
Observation 6.135 (An unsafe example in the two-thirds
interval). Write a greedy residual as
TwoThirdsBand
not_twoThirdsBand_of_int
seven_le_of_intBand_odd
Theorem 6.136 (Vanishing of the specified
linear-channel determinant). Let
Observation 6.137 (The additive error in the binary bound).
Theorem 6.94’s
Observation 6.138 (Odd denominators of finite sums). For
finite
Theorem 6.139 (Excluding the cell with value minus
three). At a middle row
Further finite and conditional results
This subsection records further finite identities and conditional
membership results. They concern the middle transition, finite families
with a common prefix, and rational targets other than
The integer update in a middle interval
The following identities explain the two-sided bound and the
reset-band condition used above. They also distinguish the signed middle
coordinate
Proposition 6.140 (The unsafe middle range is exactly
three integers). For
The complement of the two safe integer ranges is precisely
For a row
Here braces denote fractional
part. Assume
This inequality has a Lean
proof (seamMiddleCell_four_mul_floorZ_le).
On a middle transition
also proved in Lean (seamMiddleCell_scaledRationalRemainder_le).
For finalMiddleCell_neg_three_not_last.
That tail hypothesis must not be dropped. For
A parallel equivalence holds for the right branch: an overshoot
witness seamRightPulseLeak_iff_distanceCell).
The remainder left by the integer greedy rule with the row-seamPureHalfPrefixRemainder)
has an exact case-split formula (seamPureHalfPrefixRemainder_eq_ite),
and a bound on it is proved equivalent to the two-sided bound (seamPureHalfPrefixRemainder_le_iff_twoSided).
Observation 6.141 (The reset-band hypothesis has a verified
base case). The upper-reset dyadic-band escape condition (discussed
after Section 12.5) is
reduced by three lemmas to a quarter-scale overshoot exclusion: an
equivalence (seamUpperReset_band_iff_successorRemainder_avoids)
rewrites the reset-charge band as a successor-remainder avoidance; an
identity (upperResetCharge_dyadicDistance_add_abovePulse)
rescales it by a factor of seamUpperReset_band_of_overshoot_band)
derives the band from a quarter-scale overshoot exclusion plus the pulse
bound seamUpperResetDyadicBandEscape_at_thirteen).
This is one verified row of a hypothesis required for every
Finite approximations without compatibility
For a finite support
is the half-carry at the terminal rank. It is
follows by expanding each Mersenne weight. Indeed,
Here
Each finite value belongs to the closed achievement set; its limit therefore belongs too, even when the finite supports disagree. No compatibility between them is needed for this implication. The finite approximants themselves remain an unproved input. A square-root terminal bound is sufficient and stronger as a bound on these particular witnesses; it does not establish a strict logical separation between the corresponding existence statements.
Here is the finite family used in the cited construction. Put
all
The suffixes therefore have consecutive
binary values
Proposition 6.142. Every shared-prefix family
just defined at depth
Four concrete instances, at depths fullCylinderStage51_halfTerminalOnlyStripWitness,
fullCylinderStage54_halfTerminalOnlyStripWitness).
This is a finite chain of witnesses; it does not reach unbounded
depths.
Observation 6.143 (Shared-prefix families at unbounded depths). The conditional theorem
is proved unconditionally (exists_infinite_support_half_of_cofinalCylinderStages),
with a positive-support refinement using the same odd-denominator lemma
(finite_boolSupport_ne_half;
exists_infinite_positive_support_half_of_cofinalCylinderStages).
The hypothesis requires these finite families at arbitrarily large
depths and is unproved. The terminal bound then implies half-membership.
This is a sufficient condition; no converse or strict comparison with
other sufficient conditions is established here.
For the conditional implication, choose the member with terminal
carry
Removing one case from a sufficient tail condition
Five Lean declarations reduce the cases that remain to be checked in
the square-root lower bound on the producer carry at late middle rows
(discussed in Part IV), using the proved exclusion of the
Definition 6.144. The middle tail condition
is the hypothesis that at every genuine middle transition (SeamMiddleProducerTailEscape).
The reduced middle tail condition is the same hypothesis
restricted to cells SeamMiddleProducerTailEscapeExceptNegThree).
The middle tail condition trivially implies the reduced one (SeamMiddleProducerTailEscape.toExceptNegThree);
the substance is in the converse direction. The reduced condition, with
cell middleProducer_neg_three_not_last),
already suffices for half-membership:
(half_mem_mersenneAchievementSet_of_middleProducerTailEscapeExceptNegThree).
The unreduced condition and the square-root bound both imply it (half_mem_mersenneAchievementSet_of_middleProducerTailEscape).
So the square-root bound implies the middle tail condition, which
implies the reduced condition, which implies
An eventual nonnegative margin
The finite-horizon condition can be stated directly. Recall the
integer margin exists_greedyHalfFrozenMargin_nonneg_iff_excess_neg).
Definition 6.145 (A nonnegative margin by the next
depth). At every skipped step
It implies half_mem_mersenneAchievementSet_of_governedFrozenMarginProducer,
through half_mem_mersenneAchievementSet_of_skipped_dyadicCap).
Indeed, the finite coefficient window is at most its infinite tail, so
The bound
Rewriting the signed carry recurrence
Numeral-adjacent boundary words have more structure than the
previously used coefficient bound. If the lower suffix numeral is one
larger than the upper suffix numeral, there is a unique carry pivot
exists_carry_pivot_of_wordSuffixNumeral_succ).
Hence for every positive coefficient row
not merely an inequality
(supportCoeff_add_deepDivisorCount_eq_of_carry_pivot).
The stage-level theorem consumes adjacent profiled prefixes directly
(profiledGapStage_carry_pivot_of_hasAdjacentPrefixes).
This is a local normal form for the two-sheet boundary. It does not
produce adjacent stages at unbounded depths and therefore decides
neither half-membership nor universal #257.
Further restrictions on represented values
These results concern achievement-set geometry and do not settle the
universal irrationality problem. For an arbitrary support restriction
supportedMersenneAchievementSet).
It is compact (isCompact_supportedMersenneAchievementSet),
nowhere dense for every isNowhereDense_supportedMersenneAchievementSet),
and perfect, that is compact with no isolated points, whenever perfect_supportedMersenneAchievementSet),
via a Cantor-space no-isolated-point argument on the coding space itself
(preperfect_supportedMersenneDigitSet).
Proposition 6.146 (Exact Lebesgue-measure dichotomy).
Either
The finite case is an exact doubling induction over inserted
coordinates (volume_supportedMersenneAchievementSet_insert),
using disjointness of the two coordinate-split faces (disjoint_supportedMersenneAchievementSet_translate);
this is where unique binary coding is used. The dichotomy is the case of
retained coordinates of Hornich’s strict-tail measure formula [4]: the retained Mersenne
weights still exceed their tails, and the Mersenne tail estimate
supplies the values
Conditional counterexamples at rational targets
Finite supports whose scaled terminal carries tend to zero give an
infinite exists_rational_half_counterexample_of_terminalScaledVanishing),
and hence refute the universal statement (not_universal_of_terminalScaledVanishing;
the universal statement itself has its own UniversalMersenneSubseriesIrrationality).
The required finite supports have only been checked to a large finite
cutoff. This restates the open half-membership question; it is not a new
result, since any representation of
A Lean theorem also proves an unconditional finite-support
obstruction at the second rational target
for every finite
finiteErdosSum_ne_one_div_twenty_one).
The denominator-order identity forces
Multiplicity of the stated two–three representations
Consider the primitive representations IsPrimitive23Solution).
Every exists_primitive23_solution_of_eleven_le),
while no_primitive23_solution_ten).
The value exists_two_primitive23_solutions_eleven),
and so does every exists_two_primitive23_solutions_mul_ten).
These facts explain an approach and give no counterexample: nothing here
proves that the associated integer-multiplicity expansion of
Integer-quotient tests for one twenty-first
For
(one_div_twenty_one_mem_iff_not_fatalAlignedBranch).
On the fatal branch the canonical quotient remainder twentyOneFatalAlignedBranch_eventually_strict_supercapacity),
and thereafter the support appends twentyOneFatalAlignedBranch_eventually_affine_supercapacity).
Conversely, closed rows twentyOneCofinalEvenQuotientGreedyDecay_of_closedRows;
one_div_twenty_one_mem_mersenneAchievementSet_of_cofinalGreedyDecay).
We give the definitions and the complete ordinary proof, including
the rounding estimate and the agreement through rank
The
alignment in
Proof. Put
We verify the integer comparisons as well. Set
For any
If
On
Also
Subtract the contributions of
The remaining question is whether this eventual recurrence can occur
for the actual greedy word, or whether closed returns occur at unbounded
depths. Neither assertion is established here. Since no finite support
represents
IV. Scales, conditional interfaces and unresolved inputs
Finite ranges and unbounded parameters
Half-membership follows from exact rows at unbounded depths or from infinitely many greedy skips. The reset criterion has a different form: it assumes a bound at every reset beyond a threshold. We compare these quantifiers before using the shared transition identities. A finite witness cannot replace either unbounded existence or a uniform bound.
For example,
Table tab:scale-ladder records both the exact parameter ranges and the reasons for the assertions: ordinary or formal proofs, cited theorems, finite calculations and unproved hypotheses. The lower rows include proved conditional implications as well as open antecedents. Neither their truth nor their evidence is determined by the quantifier prefix alone.
Result |
Quantifier prefix |
|---|---|
Result |
Quantifier prefix |
Seed for continuation from exactLocalMersenneHalfRow_six |
|
One-point countermodel: the
double-or-recycle transition shape alone, even seeded, does not give
exact rows at unbounded depths. boundedDoubleOrRecycleModel_not_cofinal |
|
The combined-residue-mass splitFractionMass_one_bound_not_necessary_fixture |
|
Exact residual: half_sub_four_term_prefix_eq |
none (numeric instance) |
Closed-form Möbius–Lambert value tsum_moebius_div_two_pow_sub_one_eq_half |
none (closed-form value) |
The one natural negative-Möbius candidate
support overshoots: half_lt_tsum_negativeMobius |
one fixed candidate support |
From an exact row, either repeated
doubling is available or an exact row is obtained at some exactLocalMersenneHalfRow_double_or_recycle |
|
Every above-half bounded support recycles
into a genuine exact row at some exists_skippedCoreExactRow_of_value_above |
|
(A cross-check for Problem #249.) totient_series_ne_rat_of_den_dvd_upto_sixteen |
|
| Truncation-rung ladder: |
|
Membership equals greedy survival. mem_mersenneAchievementSet_iff_greedy_survival |
|
Membership iff every actually skipped rank
survives. no_lastHalfGreedySkip_iff_every_skip_survives |
|
Every crossing core is forced to be the
canonical rational half-greedy prefix. eq_halfGreedyPrefixSupport_of_critical_crossing |
|
Largest-skip conditional implication used
in the reset argument. half_mem_mersenneAchievementSet_of_largestSkipLateStepSocket |
|
Band avoidance verified by exact
computation at reset indices seamUpperResetDyadicBandEscape_through_thirty |
|
Critical-band-index reduction: a half_mem_mersenneAchievementSet_of_upperResetCriticalBandEscape |
|
Parity obstruction: no finite support has
value finite_boolSupport_ne_half |
|
Full-support irrationality at every
integer base. irrational_erdosSum_full_support;
base two: irrational_erdosBorwein_series |
|
Erdős 1968: any infinite,
pairwise-coprime, reciprocal-summable index set gives an irrational
support series. irrational_erdosSupportSeries_pairwise_coprime |
|
Block-certificate criterion, independent
of the problem: a weighted-coefficient series is irrational given a
divisibility and window certificate at every precision. irrational_coeff_series_of_weighted_coeff_block_certificates |
|
Finite greedy-prefix denominators are odd
(source of the parity boundary exclusion, §8). halfGreedyPrefixDenominator_odd |
|
The exact-row existence condition: exact
rows recur at arbitrarily large endpoints, with no coherence required
between witnesses (unproved). CofinalExactLocalMersenneHalfRows |
|
The preceding condition implies half_mem_mersenneAchievementSet_of_cofinalExactLocalRows |
given |
An equivalent membership condition: the
canonical rational half-greedy orbit itself has infinitely many positive
skips (unproved). CofinalPositiveHalfGreedySkips |
|
Infinitely many positive greedy skips
imply half_mem_mersenneAchievementSet_of_positiveHalfGreedySkips |
given |
Membership iff the greedy skip set is
infinite (equivalence proved; both sides assert unboundedly many
indices). half_mem_mersenneAchievementSet_iff_greedySkippedSupport_infinite |
the skipped support is infinite |
Seven equivalent forms of membership
(Theorem 6.32):
the integer-greedy sequence is not eventually always on branch half_mem_mersenneAchievementSet_iff_not_seamGreedyEventuallyRight |
every right-hand side asserts unboundedly many indices |
| Ladder dichotomy: either infinitely many rungs survive (#257 false, explicit limit support) or an eventual bad-rank obstruction closes only this route (ordinary argument, Corollary 8 of the truncation-rung note). | open branch (a): |
| Reset square-root escape, a sufficient all-reset hypothesis (unproved). Theorem 9.46 gives the conditional implication; the run-length comparison is discussed separately in Section 12.5. | |
Remark 7.1 (Finite checks and quantified conclusions). An earlier review examined eighteen possible implications from recorded results to the required unbounded-witness conditions. It found no such implication. This is a report about those attempts, not a theorem excluding other arguments.
For example, seamUpperResetDyadicBandEscape_through_thirty
checks reset indices
Approximations to the greedy orbit
Finite quotient procedures approximate the real greedy sequence for
Four reported calculations
Fix the weights
Truncation rung
. Replace the full weight by the -term truncation and ask whether some Boolean support hits exactly under the truncated weights. Certified for (Table tab:scale-ladder, finite ranges; Theorem 8.6–8.9 below).Seam row
. The base-4 seam recursion tracking the deviation of the integer greedy orbit from its dyadic target. Certified rows through for the reset-crossing classification, and the underlying orbit separately certified to row , with exactly one violation of the target inequality at reset rows , at (saved runs to row and to row ).Integer margin
. An exploratory, unverified scan of the integer-greedy margin out to , tracking how far the certified region sits from the danger threshold.Sharp tail margin. The rank-by-rank take/skip margin against the exact tail, checked for ranks
through : takes against skips, zero fatal skips anywhere, minimum safe-skip margin bits at rank , and the smallest reported take-margin bits at rank , where the remainder exceeds the weight . Here the margins are the base-two logarithms of the corresponding positive slack multiplied by (saved run; working note, section 8).
Proposition 8.1 (Stability of each fixed greedy
prefix). Let
Proof. At rank
Lemma 8.2 (No-ties lemma). At every rank
Proof. The two strict comparisons have different reasons: parity excludes equality with a weight, and irrationality excludes equality with the complete tail.
Take boundary excluded (parity). Write a finite Mersenne sum
as halfGreedyPrefixDenominator_odd,
itself traced to finiteErdosSum_den_odd).
Hence the residual after any finite prefix is
Skip-safety boundary excluded (irrationality). The tail past
rank irrational_erdosBorwein_series,
instantiated at
Both boundaries of the fatal interval
Remark 8.3. The hypotheses of Proposition 8.1 can be checked for
two concrete approximations. The truncated geometric weights
Successive tail truncations
Finite truncations of the geometric expansion give rational weights
and permit a finite decision procedure for each fixed truncation order
The arguments below are ordinary mathematics. The
accompanying exact integer computation rechecks the finite instances
Lemma 8.4 (Forced greedy). For every
Lemma 8.5 (Parity forces infinite support). For
every
Proof. The empty set has value zero. For a nonempty finite
set, put
Theorem 8.6 (Witness exclusion). Define the misalignment mass
Let
This excludes the specified gap for every Boolean prefix, not only the greedy prefix.
Proof. Suppose such a prefix exists and write
Here
There is no
Corollary 8.7 (Half-LCM horizon). Let
Proof. Let
The bound uses
Lemma 8.8 (Mod-12 filter,
Proof. If
Theorem 8.9 (Finite decision procedure). Call
Proof. Survival at all ranks plainly implies survival
through
Remark 8.10 (Verified truncations and the unbounded-index
question). The finite decision procedure verifies
If
Consequently, such
representations for an unbounded sequence of
Which hypotheses remain unproved
Three quantified conditions underlie the membership arguments below. We compare the available estimates with each condition, distinguishing a stronger assumption from an equivalent reformulation and a finite range from an unbounded assertion. The missing estimates remain open; these comparisons decide neither #249 nor #257.
The three #257 obligations, stated exactly
Definition 9.1 (257-reset). For every upper or
middle reset row
Definition 9.2 (257-cofinal-rows). For every half_mem_mersenneAchievementSet_of_cofinalExactLocalRows).
No coherence between the witnessing rows is demanded and none should be
assumed: the rows may be mutually incompatible; only their depths need
tend to infinity. Requiring compatibility would add a condition on the
witnesses. Whether that condition can be obtained from this existence
statement needs a separate extraction argument; it is not a strict
logical comparison merely because the witnesses are described
differently.
Definition 9.3 (257-universal). The original
question is the base-
Reading a row
Each entry identifies the available result, the assumptions needed to apply it, and the further estimate still required. A source link supports the stated declaration, not every proposed consequence in the discussion. Ordinary deductions and finite computations are identified separately.
Reset estimates and their missing hypotheses
Observation 9.4 (Remainders along a right-branch run). upperOrMiddle_within_of_two_pow_deficit.
For integers
For a run of exactly
The strict inequality uses
Observation 9.5 (The affine excess recurrence). affineRightExcess_exactIterate,
affineRightExcess_charge_lt_scaledInitial,
eventualRightTail_excess_exactIterate
(recurrence rightBranch_excess_succ_eq).
For
The source also gives
If the terminal row satisfies
Only this terminal bound is needed; no bound at every intermediate row
is required. If instead the largest omitted rank
The extra term must be
retained. Lateness of an omitted rank is not known to be equivalent to
Observation 9.6 (A bound at later rows). three_mul_remainder_lt_exactLateGap.
For
Since
Observation 9.7 (Exclusion of equality at a branch
boundary). seamGreedyFloorZ_ne_takeThreshold,
with halfGreedy_skipped_endpoint_trichotomy.
The first cited theorem excludes equality between the corrected
real-valued quotient expression and the terminal take
threshold: such equality would give a finite Mersenne sum equal to
Neither statement identifies its boundary with
Observation 9.8 (A sharper test for a fatal greedy gap). skipSafe_of_two_mul_le_three_mul,
three_mul_lt_two_mul_of_fatal,
two_le_of_fatal,
three_le_of_fatal_of_odd.
Let
This is not the exact threshold. With
The tail estimate gives
Observation 9.9 (Exclusion of a linear-width band at rows
13–30). seamUpperResetDyadicBandEscape_through_thirty.
Conclusion. At every upper reset row SeamUpperResetDyadicBandEscape,
whose full form would give half-membership by half_mem_mersenneAchievementSet_of_upperResetDyadicBandEscape,
and so refute the universal statement. Parameter range.
Proved at 18 explicit rows by exact computation checked in the Lean
kernel; the obligation needs all HalfUpperResetCriticalBand.dyadicBandEscape_iff_exists_critical.
Only
Observation 9.10 (Middle predecessors and right-branch runs).
seamMiddleBranch_nextRemainder_ge_row,
seamMiddleBranch_nextRemainder_ge_expBarrier,
SeamUpperResetDyadicBandEscape.remainder_ge_row.
Conclusion. Unconditional, uniform in
Observation 9.11 (A linear lower bound at middle
transitions). SeamMiddleProducerRowEscape,
half_mem_mersenneAchievementSet_of_middleProducerRowEscape
(via its cardinality and tail forms, Lean
source). Conclusion. If at every late middle row
(
Observation 9.12 (A square-root lower bound in the row
index). SeamMiddleProducerSqrtEscape,
its implication to the exact tail bound, half_mem_mersenneAchievementSet_of_middleProducerSqrtEscape.
Conclusion. If at every late middle row
Observation 9.13 (The remaining interval of possible integer
values). upperProducer_not_last,
middleProducer_neg_three_not_last,
finalMiddleCell_neg_three_not_last,
middleProducer_allRight_landingExcess_window,
middleThenAllRight_landingExcess_two_le.
Conclusion. Under the hypothesis of a last non-right
transition at row
The cited bounds
give
at a
hypothetical last middle transition
Observation 9.14 (Excluding three integer values). SeamTwoSidedDyadicCellEscape,
SeamTwoSidedDyadicCellEscape.step,
SeamTwoSidedDyadicCellEscape.twoSided.
Theorem 6.9
states the two needed hypotheses and their row ranges explicitly.
Excluding
Observation 9.15 (An upper bound on the remainder). SeamGreedyRemainderGapBound,
half_mem_mersenneAchievementSet_of_seamRemainderGapBound
and the cofinal implication Lean
source. The estimate
Observation 9.16 (Reported computation through row
200,000). Conclusion. Exact integer
arithmetic to row 200,000 (saved
run); branch counts
Observation 9.17 (Structure of resets after long runs).
Conclusion. At a dangerous reset
Observation 9.18 (The sign condition and growth of the
margin). Conclusion. At all 1209 observed resets, M
Observation 9.19 (Comparison of finite truncation lengths).
The exact finite procedure in Theorem 8.9 verifies the
twenty truncations
Finite quotient sums and unbounded depths
Observation 9.20 (Exact rows from a sharp capacity bound). exists_exactRowStrictUpperFill_of_skippedCoreSharpCapacity,
exactLocalMersenneHalfRow_two_mul_sub_two_of_skippedCoreSharpCapacity.
Conclusion. For any eq_halfGreedyPrefixSupport_of_critical_crossing
then identifies the core with
Observation 9.21 (A conditional induction for unbounded
depths). SkippedCoreCriticalQuotientSupply
exists_laterProtectedExactLocalMersenneRow
cofinalExactLocalMersenneHalfRows_of_criticalQuotientSupply
(ProtectedExactLocalMersenneRow;
strict progress Lean
source). Conclusion. Under the sharp-capacity
supply hypothesis below, the induction starts from the depth-six seed
and constructs exact rows at unbounded depths. A protected row is either
doubled while its real value stays below HalfGreedySkippedCriticalQuotientSupply:
Observation 9.22 (Unconditional capacity, off by one bit). localBinarySuffix_two_mul_sub_two_lt_upperHalfCapacity.
Conclusion. Unconditionally,
Observation 9.23 (Doubling extension, fails at the only
recorded seed). exists_exactRowStrictUpperExtension_two_mul_sub_one_of_exact_below;
rank two is automatic (two_mem_of_exact_localMersenneQuotient).
Conclusion.
Observation 9.24 (Consecutive-skip precritical bound). halfGreedy_precriticalSuffix_lt_of_next_skip
(used in halfGreedySkippedCriticalQuotientSupply_of_precriticalSuffix).
Conclusion. Unconditional: if halfGreedySkippedPrecriticalSuffixSupply_iff_preTake
proves the whole hypothesis equivalent to HalfGreedyPreTakePrecriticalSuffixSupply,
with
Observation 9.25 (Bounded-gap precritical bound). halfGreedy_precriticalSuffix_lt_of_future_skip_after_takenBlock
(with precriticalCrossingTax_of_futureThreshold,
sub_two_le_two_pow_sub_four).
Conclusion. Unconditional and uniform in both
parameters: skip at
Observation 9.26 (A computable horizon, not the required
horizon). exists_greedyHalfFrozenMargin_nonneg_of_excess_neg,
exists_greedyHalfFrozenMargin_nonneg_iff_excess_neg.
Conclusion. At every dyadically safe rank halfGreedy_precriticalSuffix_lt_iff_frozenMargin_nonneg,
binaryCoeffTail_eq_finiteCoeffWindow_add_shiftedTail
gives binaryCoeffTail_le
gives
Observation 9.27 (A nonnegative margin at an unspecified
horizon). HalfGreedySkippedFullShellNonnegative,
half_mem_mersenneAchievementSet_of_skippedFullShellNonnegative,
HalfGreedySkippedSeamEscape.
Open property and proved conditional implication. The
open property asks that every skipped rank
Observation 9.28 (Cofinal positive skips is the
obligation). CofinalPositiveHalfGreedySkips,
cofinalExactLocalMersenneHalfRows_of_positiveHalfGreedySkips,
half_mem_mersenneAchievementSet_iff_greedySkippedSupport_infinite,
Lean
source; positivity Lean
source. Conclusion. Cofinally many positive
rational-greedy skips
Observation 9.29 (Terminal bounds and restrictions on finite
support). HalfCarryCofinalTerminalOnlyStrip,
HalfTerminalOnlyStripWitness,
exists_infinite_support_half_of_cofinalTerminalOnlyStrip.
Conclusion. Cofinally many depths
Different restrictions. The terminal condition
permits any support inside the depth-
Missing step. Confinement of the strip witnesses to
the lower half:
Observation 9.30 (The live greedy carry and the carry of a
fixed prefix). GreedyHalfCarryCofinalStripReturn,
greedy_half_infinite_of_cofinalStripReturn,
infinite_support_half_of_mobiusCenteredHalfCarry_sqrtBound
(nonnegativity from Lean
source). Conclusion. Cofinal returns of the actual
greedy carry to the square-root strip (Theorem 6.86), or a pointwise
greedyHalfFrozenMargin_eq_actual_skip_margin),
not at depth halfGreedy_precriticalSuffix_lt_iff_futureSkipCoverage:
sharp capacity
Observation 9.31 (Above-support recycling, no growth
guarantee). exists_skippedCoreExactRow_of_value_above,
exactLocalMersenneHalfRow_of_first_localMersenne_crossing,
exactLocalMersenneHalfRow_two_mul_sub_two_of_skippedCore.
Conclusion. Unconditional: every finite above-half
support bounded by exists_seeded_bounded_double_or_recycle_model)
satisfies the same transition schema plus a seed and does not
give rows at unbounded depths. Growth is recovered only for protected
exact rows, whose invariants force
Observation 9.32 (Double-or-recycle dichotomy, proved
insufficient). exactLocalMersenneHalfRow_double_or_recycle,
boundedDoubleOrRecycleModel_not_cofinal,
exists_seeded_bounded_double_or_recycle_model.
Conclusion.
Universal support criteria and their limits
Observation 9.33 (A sufficient block-certificate condition).
irrational_erdosSupportSeries_of_weighted_coeff_certificates
(carry variant Lean
source). Conclusion.
Observation 9.34 (Rational targets and infinitely many greedy
skips). half_mem_mersenneAchievementSet_iff_greedySkippedSupport_infinite
(forward Lean
source; reverse mem_mersenneAchievementSet_of_greedySkippedSupport_infinite).
For every rational
The reverse implication holds for every real
Infinitely many skips do not mean infinitely many selected ranks:
Observation 9.35 (Finite sums exclude every rational with
even denominator). finite_boolSupport_ne_half;
the underlying parity lemma has its own finiteErdosSum_den_odd.
Conclusion.
Observation 9.36 (The denominator in the reciprocal-mass
estimate). dyadic_support_fraction_reciprocalMass_diverges_or_gt_one;
the version for general shiftedBooleanCollision_wrap_bound_of_common_multiple.
Conclusion. For
Observation 9.37 (Zero windows of a fixed support). supportCoeffZeroWindow_length_le_eps_logb.
Conclusion. For any
Observation 9.38 (Prime support and the reciprocal-sum
hypothesis). irrational_erdosSupportSeries_pairwise_coprime
(its certificates: exists_weighted_coeff_certificates_supportCoeff_pairwise_coprime).
Conclusion. For every
irrational in Theorem 1.3 of their 2025 preprint. That result is cited, not formalised here. What remains is a test of the method: replacing the global tail budget by a windowed one would ask whether this particular certificate theorem can recover the known theorem. It is no longer an open mathematical target or a claimed new route for #257.
Observation 9.39 (The two hypotheses of the sunflower
criterion). irrational_erdosSupportSeries_of_orthogonalPetalBouquet.
Conclusion. For
Different restrictions. Two gaps. (i) On the support: the bouquet class strictly generalises pairwise-coprime supports but still demands globally pairwise-coprime, summable petals; it inherits the exclusion of the primes noted in the preceding observation and adds nothing in the divisor-dense regime. (ii) On the selector: the tail-selection hypothesis must hold at every precision and is unproved.
Missing step. For the selector,
Observation 9.40 (What eventual periodicity supplies). irrational_erdosSupportSeries_eventuallyPeriodic.
Conclusion.
Scope of the hypothesis. The theorem allows every positive period and every finite starting threshold. It still requires an eventually periodic support, so it does not include all aperiodic supports covered by the other criteria in this record. Finite symmetric difference preserves eventual periodicity. Thus the finite-perturbation argument alone cannot extend this theorem to an aperiodic tail; a further hypothesis or argument is needed.
Missing step. A “locally periodic at cofinally many
scales” version;
Observation 9.41 (The reduced denominator in a gap
criterion). irrational_erdosSum_of_lcm_gap
(instances irrational_erdosSum_factorial_support,
irrational_erdosSum_two_pow_support).
Let
A sufficient irrationality condition is
The next omitted exponent is
If irrational_of_den_mul_abs_sub_tendsto_zero,
with all indices specified.
For upperHalfMersenneProduct_lower_bound
do not alone establish the proposed condition for an arbitrary support.
No such condition is proved here for the remaining dense supports.
Observation 9.42 (Rationality expressed by the integer
carry). erdosSupportSeries_rational_iff_exists_temperedCarry;
the general criterion of Theorem 6.105 has its own binaryCoeffSeries_rational_iff_exists_temperedBinaryOrbit.
Conclusion. For every temperedBinaryOrbit_eq_scaledTail
pins the orbit uniquely to
Observation 9.43 (Why unbounded carry alone is insufficient).
shifted_state_unbounded_of_infinite_support,
exists_unbounded_shifted_odd_tail_nat_state_of_support_fraction,
one_add_mul_card_le_two_mul_shifted_state.
Let
For a finite
This argument uses positivity of the next
state, not an assumed tail representation or a limit condition. A
general positive solution may also have an exponentially growing
homogeneous part. The condition
Finite subsets
Observation 9.44 (A finite-gap criterion for every target in
the convex hull). half_mem_mersenneAchievementSet_or_exists_fatal_gap,
half_mem_mersenneAchievementSet_iff_no_existsFatalHalfGap;
the exclusion for a general support has its own positiveMersenneSupportValue_ne_of_rank_gap.
For every real
Here
Conversely, the displayed gap contains no achievable value. A support
with prefix paper_general_target_gap.
Observation 9.45 (Why the signed periodic theorem still
requires periodicity). irrational_or_bpow_mul_eq_intCast_intWeightedErdosSeries_periodic,
irrational_intWeightedErdosSeries_periodic_of_coeff_nonneg_of_frequently_ne_zero.
Conclusion.
Different restrictions. Two mismatches. (i)
Periodicity of the weight is still required; this is the signed version
of the periodic-support theorem and keeps its periodicity hypothesis.
(ii) The one-sidedness clause is automatic for #257 (a
Missing step. An aperiodic version of the dichotomy;
for arbitrary
Three combined conditional arguments
Entry A has a Lean proof, and entry B is an ordinary argument about what its hypotheses would imply. The facts behind entry C, the survival equivalence of Theorem 5.10 and the one-sided certificates, are proved in Lean. None of the three establishes an unproved orbit hypothesis or decides #257.
Theorem 9.46 (A: a sufficient lower bound at every
reset). Assume that
Here is the role of the constants. Put
For
Remark 9.47 (B: rigidity of dangerous resets). For a
dangerous reset preceded by a sufficiently long pure right run,
Observation 12.9
confines the deviation at the preceding reset to at most two adjacent
integers determined by the divisor-pulse stream. Applying that
observation along a chain of
Theorem 9.48 (C: the one-sided finite decision
boundary). The equivalence of Theorem 5.10
separates two logically different kinds of evidence. A fatal greedy gap
found at a finite rank is a finite certificate that
The reset-crossing hypotheses, truncation-rung ladder, and
sharp-capacity inequalities feed sufficient conditions for membership.
They are not proved equivalent to one another, nor is failure to find
one at a given depth evidence of survival. Consequently these searches
give at most a semi-decision procedure for nonmembership of the
specific value
Four limitations of the stated implications
The following conditions are equivalent to their target statements within the specified scope. An equivalence may still be useful by exposing a quantity that is easier to estimate. What it does not supply is a proof of that estimate, or a strict weakening of the logical obligation.
Remark 9.49 (The centred-carry bound is equivalent to the
conclusion, for the greedy support only). greedy_half_infinite_of_mobiusCenteredHalfCarry_sqrtBound
and its packaged form greedy_half_infinite_of_mobiusCenteredHalfCarry_upperBound
assume the bound binaryCoeffTail_supportCoeff_le_two_sqrt_add_four),
the unconditional tail-nonnegativity lemma (binaryCoeffTail_nonneg),
and the greedy-specific fact GreedyHalfCarryCofinalStripReturn,
the former gap between the real and the integer square root is removed
by restricting cofinal witness depths to perfect squares. Any remaining
gap lies in the hypothesis itself, not in rounding.
Remark 9.50 (What the terminal carry condition proves). HalfCarryCofinalTerminalOnlyStrip
at the original strip constant is logically equivalent to
Remark 9.51 (Positive greedy skips and half-membership). As
noted above, the positivity conjunct of CofinalPositiveHalfGreedySkips
holds unconditionally, by parity and greedy nonnegativity (Lean
source). The hypothesis therefore says exactly that the greedy rule
for
Remark 9.52 (Scope discipline for the equivalence class).
Each equivalence uses its stated domain. The centred-carry upper bound
concerns the actual greedy support
Hypothesis-specific obstructions
An abstract recurrence can satisfy some identities of the greedy orbit and still violate the proposed reset bound. Such a counterexample applies to the actual orbit only after the correspondence of states has been proved. We keep these examples separate from calculations on genuine finite orbits. Additional arithmetic hypotheses may exclude the abstract counterexamples.
Throughout,
Four tested approaches to the reset estimate
Observation 10.1 (Prime steps can occur within a bounded
drift window). Route as conceived. The universal
recursion
A finite test. Use the skip set of the quotient row
Exact integer arithmetic gives, in order at
There are eleven values and ten transitions. The indices
At a
prime index the last coefficient is
Scope. Primality at some indices does not force this drift to leave a small interval immediately. The example supplies no universal run-length bound and no statistical conclusion about prime indices. It also does not exclude a proof that combines prime counts with quantitative information about the intervening divisor counts.
Observation 10.2 (Parity and perfect squares in the
recurrence). Route as conceived.
What the parity calculation says. The recurrence
implies
Scope. Restating a parity consequence of a known recurrence does not add a new independent constraint. To turn it into a run-length bound would require further information about the sizes or arrangement of the forcing terms. No argument here rules out using parity together with such information.
Use of the observation. The parity law does
constrain
Observation 10.3 (What the denominator estimate does not
give). One proposed separation argument would prevent
For
The middle inequality is strict when the
skip set is nonempty. This is an upper bound; it is not an asymptotic
formula for
Zudilin proves
This guaranteed lower bound is
eventually smaller than
Retaining only the parity of an input coefficient leaves considerable
freedom. In
Proposition 10.4 (Centred completion of
fixed-precision 2-adic data). Fix
Thus one may
prescribe the valuation and
Proof. For a single step, put
The remainder convention
The formal-source statements are fixedPrecisionTropicalNoGo,
vu_step_has_centred_completion
and vu_word_has_prefix_locked_completion.
They concern this unrestricted congruence model, not coefficients
already fixed by a divisor-count sequence. Fixed-precision data alone
cannot exclude every completion in this model. The proposition does not
show that the completion comes from a Mersenne support, satisfies
additional arithmetic relations, or belongs to the particular greedy
orbit. In particular, it is not a general obstruction to every
fixed-window argument for Problem 249 or 257.
These observations have separate scopes: a finite prime-window example, a parity consequence of a known recurrence, an insufficient denominator estimate, and a completion theorem for specified fixed-precision symbols. They do not exhaust the possible approaches to the reset estimate or force every proof to use digit-carry machinery. The next section studies that machinery because it gives explicit conditional implications, not because other methods have been ruled out.
Excluding particular final dyadic intervals
The two-sided bound
Here Erdos249257.SeamTwoSidedDyadicCellEscape
Proposition 10.5 (The upper (carries) successor needs
no exceptional-cell exclusion). Let
Indeed, the
reset identity expresses
Theorem 10.6 (
i.e.
Proof of the bound. The all-right-tail
assumption puts the terminal-augmented finite prefix strictly above
The last inequality follows by retaining the first two geometric
channels of the complete Mersenne tail. Put
The left side is an
integer, hence is at least
Scope. This excludes
Corollary 10.7 (Only
Remark 10.8 (A sufficient tail inequality and its source).
Let
This is a tail sum, not a ratio. Since Erdos249257.middleProducer_allRight_forces_carry_lt_tail.
An inequality in the opposite direction would exclude such a final middle transition. The following sufficient condition retains the exception already handled by Theorem 10.6:
Because
This is the reduced middle tail condition of Part III, and
half-membership follows from it (half_mem_mersenneAchievementSet_of_middleProducerTailEscapeExceptNegThree).
The inequality itself is not established here. Its role is a conditional
implication, not a newly identified necessary condition.
The two more concrete sufficient bounds in Theorem 6.7 imply
the tail inequality even without the exception. Their Lean forms are Erdos249257.SeamMiddleProducerCardEscape
and Erdos249257.SeamMiddleProducerRowEscape.
The cardinality condition is
It gives Erdos249257.half_mem_mersenneAchievementSet_of_middleProducerCardEscape.
No converse between these sufficient conditions is claimed.
The scalar-localisation height obstruction
Lemma 10.13 (Denominator complement survives scaling).
For
Equivalently, writing
Scope. This is elementary rational arithmetic,
independent of the problem. If
Corollary 10.14 (Mersenne specialisation). Let
The final-skip band formula, and what it does not show
Definition 10.15 (Upper-reset dyadic band escape). At
each upper-reset row
Thus Erdos249257.SeamUpperResetDyadicBandEscape.
In words: at every upper-reset row Erdos249257.half_mem_mersenneAchievementSet_of_upperResetDyadicBandEscape
gives
Proposition 10.16 (Quantifier collapse: one critical
index suffices, not
Observation 10.17 (A verified finite range of reset indices).
The linked certificate proves the condition in Definition 10.15 for each reset
index Erdos249257.seamUpperResetDyadicBandEscape_through_thirty.
Remark 10.18 (What this does not show).
Definition 10.15
is a
The finite theorem supplies no reset index beyond
For the branch convention of Theorem 5.16, direct integer
recomputation at reset-test indices
Unproved inputs for the recorded implications
The following estimates would supply inputs to particular conditional arguments. We compare each with the bounds and finite calculations already available, retaining its quantifiers and evidence basis. The comparisons leave both rational targets and the universal problem open, and do not supply a single obstruction common to all approaches.
For example, the first two weighted divisor counts after
Definition 11.1 (The short-window divisor phase). For
where
Iteration of the integer recurrence
Consequently
A nonzero
distance is at least
Reset bounds and finite weighted divisor sums
The statement needed
The first two conditions below each have a conditional implication to half-membership. No implication between them is asserted. The sign condition is weaker than a quantitative margin in its conclusion, but its relation to either membership hypothesis must still be proved.
Form (i), the reset-deviation bound. Write
Equivalently,
Form (ii), band avoidance, already proved to imply
membership. For every upper reset
(SeamUpperResetDyadicBandEscape),
with the conditional implication to membership half_mem_mersenneAchievementSet_of_upperResetDyadicBandEscape.
The dyadicBandEscape_iff_exists_critical,
and rows seamUpperResetDyadicBandEscape_through_thirty.
Form (iii), the sign of the reset deviation.
A
finite recomputation (saved
run) verifies these signs at all
Divisor residues and the changing skip set
Expanding each divisor count separates its residue conditions. This is a finite counting identity. It does not prescribe whether an eventual proof should be analytic, combinatorial, or use another method.
Lemma 11.2 (Divisor-residue form of the short-window
phase). For all
where
and the right-hand side, with an arbitrary integer
Proof.
The identity was also checked by exact rational computation at
A finite divisor cutoff makes the averaging question precise. For
integers
This is the cutoff sum of
Lemma 11.2. It is
periodic in
The mean diverges as
The same issue arises if one uses the profinite integers
There is a related residue expression in Theorem 5.15, but its index and divisor set differ:
Indeed
To keep the changing support visible, put
A phase estimate would have
to control this additional term and identify the required reset rows
before implying the reset bound. No such implication is proved here. The
scales also differ from a logarithmic-window assertion:
Finite residue expansions, divisor-sum estimates and probabilistic local estimates are possible sources of further information. None is an input already supplied here. An application must state the divisor cutoff, offset length, error at the required precision, and control on the changing skip-set sum, rather than appeal to the name of a method or to equidistribution of a different statistic.
The specific obstacle
What the cited short-interval theorems control.
Matomäki and Radziwiłł prove that a real-valued multiplicative function
bounded by
First, their conclusions hold for almost all
Second,
The required statistic is different. A central limit theorem for prime-factor counts, or an almost-all theorem for unweighted interval averages, is not by itself a bound for the distance to an integer of this dyadically weighted divisor sum. An application must state its precision, its dependence on the growing window length, and its exceptional set. The references cited above do not supply that orbitwise estimate in the form used here. This is a limitation of the proposed application, not a survey claim that every relevant local estimate is unavailable.
The countermodels in the record impose similarly specific
limitations. They concern fixed-precision residues (affineBinaryOrbit_mod_twoPow_eq),
a decoder without fresh arithmetic input (balancedPulse_no_autonomous_decoder),
and fixed-precision signatures (fixedPrecisionTropicalNoGo).
They do not partition all possible proof methods. Together with the
denominator estimate, they explain why the particular shortcuts examined
here are insufficient; they do not prove that a weighted-window method
is necessary or impossible.
Possible estimates to prove
A conditional bound along a right-branch run.
Let
The reverse triangle inequality and the finite geometric sum give
This estimate alone
does not force a right-branch run to end. For that conclusion one also
needs an upper bound on its terminal deviation. More precisely, if
then division by
Every term and hypothesis is explicit here. A separate window estimate must supply the displayed terminal upper bound; it does not follow from the right-branch recurrence alone. This explains the possible connection between the initial deviation and the run length without asserting a sharp threshold, a run-length equivalence, or an unproved bound for all later rows. This conditional calculation is an ordinary argument.
An exact finite phase experiment.
For the
| Count | |||||
| Proportion | |||||
| Proportion |
The experiment samples consecutive integers, not reset rows. Its
median distance is
Truncation matters at the smallest tested thresholds. With the same
starting indices, the counts below
Distance to the nearest
integer is
A probabilistic application requires further assumptions. For
example, if events
Summability would also imply only finitely many failures almost surely, not zero failures at every index. Neither the finite histogram nor its fit to a uniform-phase model proves these probability bounds, identifies their events with reset failures, or defines a probability for the actual deterministic orbit. In particular, no membership conclusion is drawn from small expected counts computed in such a model. The counts are exact finite computations; the error and probability inequalities are ordinary arguments; an application to resets is unproved.
The reset signs and the exact branch identities. Write
The
natural-number subtraction can be read as signed subtraction because
On an upper transition, let
This sign
already follows from the exact upper-branch identity; only the middle
sign needs further orbit information. On a right transition the
corresponding formula is
Progress to larger endpoint depths
The statement needed
The exact-row transition exactLocalMersenneHalfRow_double_or_recycle
says every exact row
where SkippedCoreCriticalQuotientSupply);
Unboundedness of
What kind of object would furnish it
The real and integer greedy rules must be distinguished here. A real
straddling word agrees with the real greedy prefix (IsStraddlePrefix.half_agrees_greedy).
An exact local row instead satisfies
One possible additional ingredient is an integer-valued function
localBinarySuffix_two_mul_sub_two_lt_criticalCapacity_iff,
form (a) is exactly the statement that the
The specific obstacle
The formal counterexample concerns exactly the transition schema:
that schema plus a seed provably does not give cofinality. The
theorem exists_seeded_bounded_double_or_recycle_model
exhibits the one-point predicate exactLocalMersenneHalfRow_six,
the explicit witness
There is a second, more specific trap, and it is also formalised. The
natural sufficient condition via fractional split mass is not
necessary: the example at splitFractionMass_one_bound_not_necessary_fixture)
exhibits a real crossing core violating it. Thus the fractional-mass
bound is not necessary for an individual crossing core. This
counterexample does not rule out proving that sufficient bound on a more
restricted family.
Possible estimates to prove
The uniquely determined prefix at a crossing. The identification below is proved; the required capacity bound remains open.
Form (a) is universally quantified over cores eq_halfGreedyPrefixSupport_of_critical_crossing,
which forces
The crossing hypothesis has not disappeared: these are the ranks where the real greedy rule skips the next term. Each resulting finite inequality is decidable. Computing its margin can identify examples to explain a proposed estimate, but a finite table neither selects a proof method nor establishes a cofinal supply.
The progress-function criterion above remains unproved. Endpoint doubling is not a proved doubling law for the largest selected exponent, and an unbounded function of the incoming endpoint alone does not rule out a bounded cycle.
Prime support and the limits of one formal argument
The base-
is known. Expanding geometrically and collecting divisors gives
and Tao–Teräväinen prove the latter series irrational in Theorem 1.3 of Quantitative correlations and some problems on prime factors of consecutive integers. This is a cited analytic result, not a theorem formalised in Lean.
The existing pairwise-coprime Lean theorem does not recover it
because that theorem assumes
a
simultaneous exact divisibility pattern far stronger than the input used
by Tao–Teräväinen. Small computational witnesses for
Thus the contribution of this analysis is negative and specific to
the method: it identifies why the present formal certificate criterion
fails to reproduce a theorem already available by quantitative
correlation estimates. The earlier proposal to prove the prime-support
irrationality as new mathematics is withdrawn. Extensions to other bases
or prime-power supports are mentioned by the cited authors with proof
modifications omitted; this paper promotes only the fully written
base-
Equivalent carry conditions at perfect-square depths
The statement needed
The following five conditions are equivalent to
for every .The set
is infinite.For arbitrarily large
there is with .For arbitrarily large
, .For arbitrarily large
there is with .
Here half_mem_mersenneAchievementSet_of_positiveHalfGreedySkips,
half_mem_mersenneAchievementSet_of_cofinalExactLocalRows,
half_mem_mersenneAchievementSet_of_cofinalStripReturn,
half_mem_mersenneAchievementSet_of_cofinalTerminalOnlyStrip).
The reverse implications are ordinary deductions in this paper. The
perfect-square argument below supplies the terminal bounds without
changing the constant in the original statements.
The carry bound at perfect-square depths
Lemma 11.3 (The terminal bound at square depths).
Let
Proof. By integerHalfCarry_eq_scaled_residual_add_tail,
and the first term vanishes by
hypothesis. Take binaryCoeffTail_supportCoeff_le_two_sqrt_add_four
(unconditional) the tail at halfStripBound,
binaryCoeffTail_nonneg)
gives the lower side. ◻
The difference between the real and the integer square root
disappears when cofinal witness depths are restricted to perfect
squares: at integerHalfCarry_inter_Iic_eq_of_succ_le
together with HalfTerminalOnlyStripWitness
and hence (5).
What the equivalences establish
Each biconditional is a theorem about the exact logical content of a proposed hypothesis. It is also a reformulation of the membership question. These are compatible descriptions, not competing evidence classes. The equivalence identifies the missing content but does not show that the reformulation cannot expose a useful invariant. In particular, (3) shows that the existence of finite witnesses at unbounded depths, even without compatibility between those witnesses, is equivalent to membership. The absence of a compatibility requirement may still be useful in constructing witnesses; equivalence alone says nothing about which formulation is easier to prove.
Scope of the equivalences. (1) does not
extend to every erdosSupportSeries_greedyMersenneSupport_le
(which supplies mem_mersenneAchievementSet_iff_greedy_survival.
Sparse and dense supports under the certificate criterion
The statement needed
For a fixed nonempty supportCoeffZeroWindow_length_le_eps_logb
does not create a sparse subclass here. The separate lcm-gap theorem irrational_erdosSum_of_lcm_gap
remains a valid sufficient criterion, but does not prove this proposed
alternative. The proposal would consequently require the following
certificates for every infinite support:
What kind of object would furnish it
The identity
Necessity
follows by subtraction. For sufficiency, keep the strongest prime-power
modulus for each prime; compatibility makes all weaker prescriptions
agree with it, and the ordinary CRT combines the resulting coprime prime
powers [23]. For
example,
The specific obstacle, proved
The dense branch as stated is false: an explicit, natural, divisor-dense support refutes it. This also corrects an earlier claim that universal #257 reduces with no loss to the existence of certificates for every infinite support.
Proposition 11.4 (Squarefree support: a limit of the
certificate method, not an open value). Let
which is
odd for every
This does not leave the squarefree value open. Duverney–Tachiya’s
Corollary 1.2 and Example 1.1 prove that, for every
are linearly
independent over
The dependence on the choice of support is exact. Adjoin ErdosProblems.Erdos257.supportCoeff_squarefreeShiftedSupport
and ErdosProblems.Erdos257.irrational_erdosSupportSeries_squarefreeSupport_iff_shifted.
At base ErdosProblems.Erdos257.exists_omega_ge_block
and ErdosProblems.Erdos257.exists_digitwise_block_squarefreeShiftedSupport.
The middle-window and height conditions remain; no certificate or new
irrationality proof follows. The durable conclusion is methodological:
test a no-go statement under rational finite changes before attributing
it to the underlying value.
What the experiments and obstructions do not imply
Everything in this subsection is inference from the recorded failures, not a theorem. Where the evidence does not determine the answer, the text says so.
Finite observations and their limits
The recorded obstructions concern specified representations. Fixed
precision, a bounded carry state and a prescribed suffix can lose
information needed by the actual-selector condition. They do not show
that the underlying deterministic sequence has no arithmetic structure.
The relevant exact statements remain fixedPrecisionTropicalNoGo,
balancedPulse_no_autonomous_decoder
and affineBinaryOrbit_mod_twoPow_eq.
Their hypotheses, rather than the fact that an attempted argument
failed, determine their scope.
The inherited experiment log reports
The exceptional row
These representations all descend from the same greedy carry; they are not independent tests of a common random hypothesis. Strict tail domination gives an injective coding, but says neither that its digits are random nor that averaging over indices is impossible. The measure-one and nowhere-dense properties of the achievement set do not decide membership of a specified rational. The correct research question is whether a precise arithmetic estimate can be proved for the actual selector, not whether finite data resemble a random model.
Why the support and rational-target problems remain distinct
Proposition 11.4 is a reason to
separate the two halves rather than assimilate them. On the universal
side the present certificate method first meets a parity obstruction
that depends on the choice of support. The squarefree value is
nevertheless already known to be irrational at power-of-two bases, and
adjoining
Short-window near-integer anti-concentration is one possible missing input for the particular mechanisms analysed here. No equivalence shows that it is necessary for either problem, and no argument identifies it as a common necessary obstruction to both. The squarefree example shows why finite rational changes of support must be checked before an opening-block failure is interpreted as a property of the value.
What the evidence does and does not determine
It does not determine whether a short proof exists: nothing in a catalogue of failed methods bounds the length of a successful one.
It records limitations of specified methods. The fixed-precision
completion theorem and the balanced-pulse countermodel concern the
particular summaries defined above, not all fixed-precision arithmetic
or all finite-state methods with additional arithmetic input. An
irrationality-measure bound on
V. Outstanding obligations and provenance
What is open, stated exactly
The support theorems and finite arithmetic leave three target
questions: the universal base-two assertion, half-membership and
Notation fixed for this section
The base-erdosSupportSeries).
supportCoeff)
is the divisor-indicator coefficient whose generating tail enters every
certificate below. mersenneAchievementSet).
The universal statement
Definition 12.1 (Universal #257).
This is the literal statement of Erdős #257; it is open. The sufficient condition used by the certificate method of this record is
with irrational_erdosSupportSeries_of_weighted_coeff_certificates;
the theorem is universally quantified over
would imply ErdosProblems.Erdos257.not_exists_digitwise_certificates_squarefreeSupport).
This is a limit of the method, not a counterexample to irrationality:
Duverney–Tachiya prove the squarefree value irrational at every
power-of-two base. Likewise the pairwise-coprime theorem does not cover
the primes because
Whether one half is represented
Definition 12.2 (Half membership).
finite_boolSupport_ne_half;
finite supports have odd-denominator value, so can never equal a dyadic
rational), hence a genuine counterexample to
(half_mem_mersenneAchievementSet_iff_greedySkippedSupport_infinite;
the reverse direction holds for every target, and the forward direction
uses only that the target is rational, so the same theorem holds
verbatim for every rational
Conditions equivalent to half-membership
The following three conditions are equivalent to half-membership. They express the same unresolved assertion in different terms. The proofs of equivalence identify the content still to be established; they do not compare the difficulty of possible proofs.
Proposition 12.3 (Infinitely many positive skips are equivalent to half-membership). Define
The positivity
conjunct is unconditionally true for every skipped
The implication cofinalExactLocalMersenneHalfRows_of_positiveHalfGreedySkips
therefore gives an equivalent formulation, not a proof of
membership.
Proposition 12.4 (Terminal carry bounds are
equivalent to half-membership). Consider finite sets
This is the exact terminal-strip condition. It is
equivalent to
The existence condition is therefore not logically weaker than half-membership. An equivalent formulation may still be useful for finding a proof.
Observation 12.5. Propositions 12.3 and 12.4 do not decide
half-membership. They show that the proposed existence conditions are
equivalent to it, not that those formulations have no possible use. The
upper bound on the centred carry in greedy_half_infinite_of_mobiusCenteredHalfCarry_sqrtBound
has the same equivalence for the greedy support
Exact finite sums at unbounded depths
Definition 12.6. For every integer
(CofinalExactLocalMersenneHalfRows).
This condition is unproved. Supports at different depths need not agree.
This is the condition in Definition 6.66; no strict
weakening of half-membership is asserted.
The implication from this condition to half_mem_mersenneAchievementSet_of_cofinalExactLocalRows).
The cited theorem already proves that a representing support exists,
because that is what membership of continuous_positiveMersenneDigitValue.
The diagonal argument preserves two_mem_of_exact_localMersenneQuotient).
This describes an ordinary existence proof; no additional formal
extraction theorem or effective algorithm from purely existential row
data is claimed.
Proposition 2.7(c) already
identifies this condition as logically equivalent to
A capacity condition for exact sums at unbounded depths
The finite construction uses a
(localBinarySuffix),
with natural-number subtraction understood as truncated at zero. The
loose bound below requires a critical crossing:
The implication localBinarySuffix_two_mul_sub_two_lt_upperHalfCapacity).
localBinarySuffix_two_mul_sub_two_lt_criticalCapacity_iff
(under the stated core hypotheses), is equivalent to
The excluded band contains
The sharp-fill implication exists_exactRowStrictUpperFill_of_skippedCoreSharpCapacity
assumes
The complete induction from the endpoint-six seed to exact sums at
unbounded depths is already formalised (cofinalExactLocalMersenneHalfRows_of_criticalQuotientSupply);
it uses the sharp capacity input, in its reduced canonical form
(HalfGreedySkippedCriticalQuotientSupply),
at essentially every step; this input is unproved. This condition is
required along the specified greedy prefixes. That restriction on the
witnesses does not by itself prove a strict logical ordering with the
cofinal condition above.
Reset bounds and runs of right transitions
Definition 12.7 (Reset
The conditional implication uses the integer bound
The last implication is half_mem_mersenneAchievementSet_of_largestSkipLateStepSocket;
the first is proved in Theorem 9.46. These
are sufficient implications, not an equivalence with
half-membership.
For comparison one may ask for
where
The pulse sum and
the threshold ranges cannot be dropped to claim
Finite evidence. Exact integer arithmetic to row
Observation 12.8 (The sign of the reset deviation). At all
Observation 12.9 (Rigidity of dangerous resets). If reset
Three middle-cell exclusions and the right-branch bound
Definition 12.10. The two-sided cell
condition excludes three integer values of the middle coordinate,
SeamTwoSidedDyadicCellEscape).
Granted this, induction from a base case at row SeamTwoSidedDyadicCellEscape.twoSided,
given the hypothesis). The final-middle theorem excludes finalMiddleCell_neg_three_not_last).
It does not supply the
Here
A distinct sufficient condition concerns upper resets only. For every
This is the upper-reset band condition
of Theorem 6.10 (SeamUpperResetDyadicBandEscape).
It is unproved in general, and verified by exact finite computation for
rows seamUpperResetDyadicBandEscape_through_thirty).
This band has linear width half_mem_mersenneAchievementSet_of_upperResetDyadicBandEscape).
It is proved logically equivalent to a single-critical-index check per
row (seamUpperResetCriticalBandEscape_iff),
which is a genuine quantifier-complexity reduction, not a strength
reduction.
Whether one twenty-first is represented
The integer-quotient proof at the end of the detailed finite results gives the equivalence
(one_div_twenty_one_mem_iff_not_fatalAlignedBranch).
The fatal branch twentyOneFatalAlignedBranch_eventually_strict_supercapacity
and twentyOneFatalAlignedBranch_eventually_affine_supercapacity.
Any unbounded sequence of closed returns instead proves membership.
No finite support on ranks at least finiteErdosSum_ne_one_div_twenty_one).
Thus membership would already be an infinite-support rational
counterexample to
Implication table
Read left to right:
Target |
Relation to its endpoint | Status |
|---|---|---|
| Universal irrationality | Would exclude both rational targets; the stronger universal certificate condition is false | open |
| Half-membership | Would give a counterexample to universal irrationality | open |
| Equivalent to excluding the specified failure branch; would give a counterexample | open | |
| Infinitely many greedy skips (Proposition 12.3) | open, equivalent condition | |
| Terminal-only strip (Prop. 12.4) | open, equivalent condition | |
| The centred square-root bound for |
open, equivalent condition | |
| Exact finite sums at unbounded depths | open, equivalent condition | |
| Linear-width capacity band | open | |
| The quotient condition on skipped greedy prefixes | open; no strict comparison asserted | |
| Reset square-root bound | open | |
| The reset sign condition | no implication to half-membership stated | open |
| Rigidity after long runs | partial rigidity, no exclusion | open |
| The remaining middle-cell exclusions and right-branch bound | open | |
| The upper-reset band condition | open; verified for |
Possible inputs and their scope
The following comparisons identify missing hypotheses in the recorded arguments. They neither predict the length of a proof nor classify all possible methods.
The universal statement. The question is
Half-membership, exact sums and middle cells. The
sharp-capacity gap
Reset separation. The specified quotient-row
argument needs
Summary
The results here do not decide the universal statement
Logarithmic cost under arithmetic sampling
A logarithmic divisor majorant is too weak to give the uniform arithmetic-progression estimate suggested by the fractional-cover proof. We construct a counterexample already visible on complete periods, so an improved incomplete-period error cannot remove it. We then prove an initial-interval estimate. This distinguishes the available logarithmic bound from a converse to the short paper’s divisor-cube estimates.
The ordinary proofs originate in an AI-assisted note of 17 September
2026. The margin gives the three corresponding formal results and their
separate comparison records. The ordinary proofs have not had
independent human review. For the underlying Lambert subseries,
Kovač–Tao treat the same fixed-base object in [19]; their strict-tail argument gives distinct
support coding and Cantor topology. Van Doorn–Kovač treat a freely
chosen denominator sequence. Their convention is
The two finite costs
Let
For
The constraints also hold at every positive
integer
We use
over finite or countable families of finite sets
Theorem 13.1 (arithmetic logarithmic counterexample).
For every integer
For these
uniformly in finite
Proof. We choose the modulus so that several small divisibility conditions hold automatically. Fresh tag primes make the remaining conditions independent. Taking all least common multiples then makes the divisor count exponential in the number of tags. Its logarithm has small cost, but the shifted potential exceeds one at sufficiently many offsets to prevent the proposed uniform bound.
Choose a finite set of primes
we have
Thus the set
Choose a finite set
Divergence of the prime reciprocal sum
after any finite cutoff permits stopping at the first crossing of
The same
stopping argument works successively: each new reciprocal is less than
Let
where the least common
multiple of the empty set is one. Every tag prime occurs in just one
labelled pair. Its presence in the least common multiple therefore
recovers whether that pair was selected. Hence different subsets give
distinct exponents. All exponents are squarefree; different parent
primes give disjoint sets, since no parent prime occurs in any other
set. Their minimum is greater than
For an integer
Indeed, when
All moduli in this majorant divide
Now sample
and its variance is at most
Thus success has conditional
probability at least
Different parent
groups depend on disjoint prime coordinates, so the
Since
Since
Summing over the dyadic window gives
Take
The arithmetic lower bound for every fractional cover
Corollary 13.2 (finite-functional separation).
For every finite nonempty
where
Proof. Fix one finite-cost cover in (18), and
write
Nonnegative
interchange and the original geometric-kernel estimate (13), with
its factor
Keep the cover
and
What survives without arithmetic restriction
Proposition 13.3 (ordinary initial intervals).
For every finite nonempty
Proof. Choose a positive logarithmic divisor majorant
If
a contradiction. If
Take the infimum over the admissible majorants. ◻
The proposition also bounds every
Two proof details and sources
The comparison of displacement atoms works for real bases:
For the scalar positive-cover cost, put
These two calculations supply the elementary details used in the short paper.
The original periodic and linear-independence papers of Luca and Tachiya are now distinguished from their later overview [14][15][3]. Their theorem formulations used here were read in the author-written overview; the two original publisher PDFs were not retrieved. Van Assche’s nonvanishing and small-linear-form argument for the full Lambert series [16] is a comparator for the missing upper-height control, not a result for arbitrary thinnings.
For achievement-set background, Hornich’s original bibliographic record [17] is separated from the exposition actually used here [4]. Głąb and Prus-Wiśniowski’s survey [18] provides a modern map of geometry and cardinality questions, not a rational-membership theorem for the present set.
Library declarations.
The following fixed-revision links locate the supplementary formal
statements used in this note and its companion. Pairwise-coprime
supports: factorial-support
instance; powers-of-two-support
instance; pairwise-coprime
theorem. Eventually periodic weights: irrationality
for the stated eventually periodic weights. Fixed-core supports: carry
certificates for the stated fixed-core support; irrationality
for the stated fixed-core support. Finite supports and denominators:
noncollapse
for the reduced rational denominator. Rational values and carries:
rational
support values and Möbius-inverted carries; rationality
and integer recurrences with vanishing scaled error; a
lower bound for reciprocal mass; unboundedness
of the shifted odd-tail recurrence; lengths
of intervals with zero divisor count. Composite dilation: the
divisor-count identity under dilation; the
upper bound for the dilation correction; the
example with exponents two and six. The achievement set: Lebesgue
measure one; perfect;
totally
disconnected; nowhere
dense; membership
and greedy tail bounds; non-membership
of
Verification and reproducibility
Links marked Lean source identify the
declaration associated with a statement or proof step. The
integer-quotient proof for
Statements and declarations
Artefact and data availability.
The Lean declarations, fixed toolchain and library versions are given in the evidence record linked above.
Scope of the formal checks.
Kernel checking establishes that a proposition was proved; it does not validate the exposition or the literature judgements, and it does not solve Problem 257.
Funding and competing interests.
This work received no external funding. The author declares no competing interests.
References
P. Erdős, On arithmetical properties of Lambert series, J. Indian Math. Soc. 12 (1948), 63–66.
P. Erdős, On the irrationality of certain series, Math. Student 36 (1968), 222–226 (issued 1969); five-page scan. The theorem on p. 222 treats pairwise-coprime support with convergent reciprocal sum at every integer base
; the claimed removal of pairwise coprimality is stated without proof. The same page says the reciprocal-sum condition could be replaced by a weaker but more complicated condition, and p. 226 suggests for pairwise coprime supports.F. Luca and Y. Tachiya, Linear independence results for the values of divisor functions series, RIMS Kôkyûroku No. 2014 (2017), 138–150. Theorem A (p. 139) restates Theorem 1.1 of their paper Irrationality of Lambert series associated with a periodic sequence, Int. J. Number Theory 10 (2014), no. 3, 623–636, DOI: for a purely periodic integer sequence
, not identically zero, is irrational for every integer with . Example 2 (p. 140) treats the odd support.Z. Nitecki, Subsum sets: intervals, Cantor sets, and Cantorvals, arXiv:1106.3779v2 (2013). Theorem 4 (p. 9) shows that when every term exceeds its tail the subsum set is a Cantor set of Lebesgue measure
, where is the th tail, and credits this to H. Hornich (1941).N. Sedaghat, T. Stephen, and L. Chindelevitch, Speeding up dualization in the Fredman–Khachiyan Algorithm B, 17th International Symposium on Experimental Algorithms (SEA 2018), LIPIcs 103 (2018), 6:1–6:13.
H. Kaneko, Y. Suzuki, and Y. Tachiya, Refinements of Erdős’s irrationality criterion for certain sparse infinite series, arXiv:2601.20743v1 (2026). The averaged tail
, a sum over offsets , is (1.7) and Theorem 1 is on p. 3; its rational-integer form, Theorem 3, is on p. 5. Lemma 1 (pp. 6–7) derives irrationality from arbitrarily small nonzero scaled tails, and Lemma 2 (pp. 7–8) shows that most scaled tails in a range are small under a counting condition on the support. Their criteria assume sparse coefficient supports.D. Duverney and Y. Tachiya, Refinement of the Chowla–Erdős method and linear independence of certain Lambert series, Forum Math. 31 (2019), no. 6, 1557–1566, DOI. Page numbers refer to the linked author preprint. Theorem 1.1 (pp. 2–3) is the refined Chowla–Erdős criterion; its proof in Section 2 (pp. 5–7) selects an index by minimising a local coefficient mass along an arithmetic progression, (2.3)–(2.9). Corollary 1.2 gives the general
theorem and its monomial images under , and at every integer base when ; Example 1.1 gives the joint squarefree family at all bases , . Both are on p. 4, which also relates Corollary 1.2 to the conjecture of Erdős and Graham; the proof of Corollary 1.2 is on pp. 10–11.T. Tao and J. Teräväinen, Quantitative correlations and some problems on prime factors of consecutive integers, arXiv:2512.01739v2 (submitted December 2025, revised April 2026). Theorem 1.3 (p. 4) proves
irrational, settling the prime-support case of #257 at base ; the paragraph after it states that the prime-support result extends to every integer base , and separately that full prime-power support is irrational at base . The modifications for those two assertions are left to the reader; arbitrary subsets of the primes or prime powers are not treated there. Theorem 3.1 is on p. 24, and the proof of Theorem 1.3 is Section 5, pp. 44–56.W. Zudilin, Heine’s basic transform and a permutation group for
-harmonic series, Acta Arith. 111 (2004), no. 2, 153–164, DOI. Theorem 1 (p. 154) gives for , uniformly in the integer with ; the remark at the end of Section 3 (p. 159) corrects the computation of the author’s earlier paper.J. M. Campbell, On the binary digits of the Erdős–Borwein constant, arXiv:2605.24160v1 (2026). Theorem 1 (p. 12) proves that the block
11occurs infinitely often in the binary expansion of , answering a question of Crandall recalled in the introduction.K. Matomäki and M. Radziwiłł, Multiplicative functions in short intervals, Ann. of Math. (2) 183 (2016), no. 3, 1015–1056, DOI. Page numbers refer to arXiv:1501.04585v4.
A. P. Mangerel, Divisor-bounded multiplicative functions in short intervals, Res. Math. Sci. 10 (2023), no. 1, Paper No. 12, DOI. Page numbers refer to arXiv:2108.11401v2.
Y.-C. Sun, The critical-window profile for the
-fold divisor function in almost all short intervals, arXiv:2401.08432v3 (2026).F. Luca and Y. Tachiya, Irrationality of Lambert series associated with a periodic sequence, International Journal of Number Theory 10 (2014), no. 3, 623–636. doi:10.1142/S1793042113501121.
F. Luca and Y. Tachiya, Linear independence of certain Lambert series, Proceedings of the American Mathematical Society 142 (2014), no. 10, 3411–3419. doi:10.1090/S0002-9939-2014-12102-2.
W. Van Assche, Little
-Legendre polynomials and irrationality of certain Lambert series, The Ramanujan Journal 5 (2001), 295–310. doi:10.1023/A:1012930828917; arXiv:math/0101187v1.H. Hornich, Über beliebige Teilsummen absolut konvergenter Reihen, Monatshefte für Mathematik und Physik 49 (1941), 316–320. doi:10.1007/BF01707309.
S. Głąb and F. Prus-Wiśniowski, Achievement sets – current results and open problems, arXiv:2512.17285v1 (2025), preprint. https://arxiv.org/abs/2512.17285v1.
V. Kovač and T. Tao, On several irrationality problems for Ahmes series, Acta Math. Hungar. 175 (2025), no. 2, 572–608, DOI. Page numbers refer to arXiv:2406.17593v4. Remark 4.1 (p. 13) records the strict tail inequality and the Cantor structure. Theorem 2.3 (p. 5; proof pp. 13–14) constructs rational merged sums from several bases under its mass hypothesis; the construction merges several bases and leaves fixed-base #257 untouched.
W. van Doorn and V. Kovač, Lacunary sequences whose reciprocal sums represent all rational numbers in an interval, Acta Arith. 223 (2026), 275–295, DOI. The theorem and page references used here refer to arXiv:2509.24971v3 (3 December 2025), https://arxiv.org/abs/2509.24971v3. Theorem 1 is on p. 2; Lemma 4 and Corollary 5 are on pp. 5–7.
P. Erdős, Some problems and results on the irrationality of the sum of infinite series, J. Math. Sci. 10 (1975), 1–7.
K. Barreto, J. Kang, S.-H. Kim, V. Kovač, and S. Zhang, Irrationality of rapidly converging series: a problem of Erdős and Graham, arXiv:2601.21442v3 (2026), to appear in Bull. London Math. Soc.
K. Conrad, The Chinese remainder theorem, expository notes, Theorem 3.1 (pp. 2–3). The compatibility criterion for noncoprime moduli used above is obtained by the displayed prime-power reduction.
P. Erdős, Beweis eines Satzes von Tschebyschef, 1932, pp. 194–198, especially §§4–5.