Reciprocal Mersenne Subseries

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.

1. Reset-deviation bound. For every upper or middle reset row $r\ge 10$, require $|\mathrm{rem}(r+1)-2^{r+1}|>2^{(r+5)/2}$. 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.

2. Band avoidance at resets, already proved to imply membership. For every upper reset $d\ge 13$ (branch $\mathrm{U}$ of Theorem 5.16) and every $j\le d$, the reset charge $4\cdot \text{overshoot}+\text{abovePulse}$ avoids the linear-width band $(2^{d-j+1}-2(d+j),2^{d-j+1}]$.

3. Sign law alone. At every reset, M-resets have $\mathrm{dev}>0$ and U-resets have $\mathrm{dev}<0$. 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 $\mathrm{\forall }j\in [0,d]$ band check to one nearest-boundary index per row; finite verification 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 $1.1119$ bits at row $14$ and about $1246$ bits at row $2500$; the reported mean is $627$ bits. These are finite observations, not a proof of an asymptotic lower bound or of the inequality at every later reset.

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 $19$ after the reset at row $\mathrm{158,096}$, far below the proposed threshold $(r-3)/2=\mathrm{79,046.5}$ there. Observing larger runs at larger ranks does not refute the existence of some uniform finite bound. Neither a uniform bound nor the weaker asymptotic assertion $L_r=o(r)$ is proved by these data. The stated implication needs the required inequality beyond the verified initial ranks.

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:

1. critical quotient supply: for every below-half core $D$ bounded by $[2,c)$ with genuine crossing deficit, $2^{(2c-2)-1}\le Q(\mathrm{insert}cD)(2c-2)$;

2. a direct proof that the crossing rank $c$ produced by the recycle branch cannot repeat the value $4$, or any bounded value, infinitely often;

3. a growth law for $c$ as a function of the incoming endpoint $n$.

By Proposition 2.2(ii), form (a) need only be checked along the one canonical orbit, the half-target greedy prefix, not searched over $D$; and by the recorded sharp-capacity biconditional it is exactly the $c-2$ bit capacity test $SD1(2c-2)<2^{c-2}$. The example $D=\{2,3\}$, $c=5$ shows that the fractional-mass sufficient condition is not necessary. It does not rule out proving that condition for a suitably restricted family.

Sources. exactLocalMersenneHalfRow_double_or_recycle; the formal counterexample exists_seeded_bounded_double_or_recycle_model (the model $n\mapsto (n=6)$ satisfies the seed and the exact transition shape yet is not cofinal, so the schema plus an endpoint-six seed provably does not give cofinality); conditional strict progress 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 $\{2,3,6\}$ at 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 $n\ge 2$,

form a decreasing sequence in which each weight exceeds the sum of all later weights by at least $1$. Apply the integer greedy rule with capacity $2^{n-1}-1$: visit $d=2,\dots ,n$ and subtract $q_{n,d}$ when it fits. By Theorem 6.100 and Propositions 6.101–6.102, any exact-row witness has zero remainder and must be this greedy word. Thus there is at most one witness at a fixed depth, and its existence is tested by checking whether the final greedy remainder is zero. An exhaustive search over $2^{n-1}$ subsets is unnecessary.

This integer greedy word should not be silently identified with the real greedy prefix $G\cap [2,n]$: the two rules use different weights. The separation theorem proves uniqueness within the integer problem, not that identification.

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-$2$ prime-support value is not an open target:

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 $\sum _{p}1/p$. That is a boundary of this certificate theorem, not a boundary of the mathematics. A windowed-tail repair of that theorem can test whether the Lean certificate theorem reproduces the known theorem; reproducing a cited result is not new progress on #257. After Theorem 1.3 the authors state the prime-support extension to every integer base $b\ge 2$ and, separately, the full prime-power result at base $2$, leaving those modifications to the reader. These statements should not be combined into an attributed all-base theorem for arbitrary prime-power subsets.

Equivalent membership conditions

Proposition 2.7 lists the equivalent conditions: a pointwise upper bound on $C_G$, infinitely many skipped ranks, exact quotient sums at unbounded depths, and the two cofinal carry bounds. For the carry conditions, the residual identity and its tail estimates are the relevant inputs: 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 $a_0=minA$, every run of zeros has length at most $a_0-1$, since each $a_0$ consecutive integers contain a multiple of $a_0$. The logarithmic estimate 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 $2^K\mid \sum _{r=1}^K{c}_A(N+r)2^{K-r}$, a bounded middle contribution $C$, and $q(C+N+L+2)<2^L$.

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.