Reciprocal Mersenne Subseries

Observation 9.4 (Remainders along a right-branch run). upperOrMiddle_within_of_two_pow_deficit. For integers $s\ge 5$ and $k\ge 0$, the cited theorem assumes $\mathrm{rem}(s)\le 2^s$ and $2^k(2^s-\mathrm{rem}(s))\ge 2^s$ and gives an upper or middle transition at some $t\in [s,s+k]$. Its literal contrapositive concerns all $k+1$ transition indices in that closed interval.

For a run of exactly $k\ge 1$ right transitions, at indices $s,\dots ,s+k-1$, a direct recurrence gives the sharper conventionally indexed statement. Put $D_j=2^{s+j}-\mathrm{rem}(s+j)$ and $p_j=p_{s+j}^{-}\ge 0$. The right-branch identity yields

The strict inequality uses $k\ge 1$, and the last bound uses $\mathrm{rem}(s+k)\ge 0$. Hence $D_0<2^{s-k}$. In particular, $D_0\ge 1$ excludes $k\ge s$ consecutive right transitions. A stronger lower bound on $D_0$ shortens that run, but must be established at the starting row of the run. Applying this argument after a reset requires the post-reset index and the deficit-side condition; it does not prove the absolute reset bound on both signs.

Observation 9.5 (The affine excess recurrence). affineRightExcess_exactIterate, affineRightExcess_charge_lt_scaledInitial, eventualRightTail_excess_exactIterate (recurrence rightBranch_excess_succ_eq). For $k$ right transitions from row $S\ge 5$, let $X_j=\mathrm{rem}(S+j)-2^{S+j}$ and $p_j=p_{S+j}^{-}$. The cited identity is

The source also gives $0\le p_j\le 2(S+j-2)$. Thus the following consequences are ordinary deductions from the identity:

If the terminal row satisfies $\mathrm{rem}(S+k)<2^{S+k+1}$, then

Only this terminal bound is needed; no bound at every intermediate row is required. If instead the largest omitted rank $d$ at the terminal row satisfies $2(S+k)<3d$, the next entry gives the different bound

The extra term must be retained. Lateness of an omitted rank is not known to be equivalent to $\mathrm{rem}(s)<2^{s+1}$; the cited estimate alone does not imply that sharper ceiling. Neither upper bound supplies the missing lower bound on an actual reset deviation.

Observation 9.6 (A bound at later rows). three_mul_remainder_lt_exactLateGap. For $s\ge 5$, if $d$ is the largest omitted rank and $2s<3d$, the cited theorem gives

Since $s-d<s/3$, its additive error is at most $(2\cdot 2^{2s/3}+4)/3$, hence $O(2^{2s/3})$. The undivided error $24^{s-d}+4$ need not be less than $2^{2s/3}$: already $s=7,d=5$ gives $36>2^{14/3}$. These numbers test the numerical estimate, not an asserted pair on the greedy orbit. The theorem supplies an upper bound only under the largest-omitted-rank and lateness assumptions. When it is used in the preceding recurrence, its additive error remains part of the result.

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 $1/2$, contrary to denominator parity. The second classifies the signed integer position of a real greedy prefix at a skipped rank; its statement explicitly permits the zero-position case.

Neither statement identifies its boundary with $\mathrm{rem}(r)=2^r$. They therefore do not, by themselves, prove $|\mathrm{rem}(r)-2^r|\ge 1$. Integrality gives that inequality only after nonvanishing of this particular deviation has been proved. An estimate of the form $2^{r/2+o(r)}$ would not settle the required constant either: $2^{r/2}/r$ has that form but is smaller than $2^{(r+5)/2}$. The reset hypothesis requires its stated constant, strict inequality and post-reset index, not merely an exponent approaching $1/2$.

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 $k\ge 1$ be a skipped rank and write its positive rational remainder in lowest terms as $\rho =u/(2L)<w_k$, with $u,L$ odd and positive. Set $a=2L-(2^k-1)u>0$. The cited sufficient condition $2u\le 3a$ guarantees $\rho <R_k$ and improves the simpler condition $u\le a$. Its contrapositive gives $3a<2u$ at a fatal skip, and hence $u\ge 3$ when $u$ is odd.

This is not the exact threshold. With ${\theta }_k=R_k^{-1}-(2^k-1)$, direct rearrangement gives

The tail estimate gives ${\theta }_k<2/3$ and ${\theta }_k\to 2/3$; $2u\le 3a$ is therefore sufficient, not necessary. For example, at $k=2$ the local rational state $\rho =77/282$ has $u=77$, $L=141$, $a=51$, so $2u>3a$, yet $\sum _{j=3}^{12}(2^j-1{)}^{-1}>77/282$ proves $\rho <R_2$. This is a local state, not an asserted point of the half-greedy orbit. Improving a bounded tail ratio alone does not provide a lower bound growing exponentially in $k$ on an arithmetic numerator; such a bound would require additional information about the actual prefix.

Observation 9.9 (Exclusion of a linear-width band at rows 13–30). seamUpperResetDyadicBandEscape_through_thirty. Conclusion. At every upper reset row $d$, $13\le d\le 30$, the reset charge $E_d=4\cdot {\mathrm{overshoot}}_d+{\mathrm{abovePulse}}_d$ avoids the linear-width band $(2^{d-j+1}-2(d+j),2^{d-j+1}]$ for every $j\le d$; the finite segment of 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 $d\ge 13$. The excluded band has width $O(d)$, whereas the reset condition uses a width of order $2^{(r+5)/2}$. This is a comparison of numerical scales, not a proof that one hypothesis on the orbit implies the other. Missing step. A structural lower bound on the distance from $E_d$ to the nearest dyadic power at or above it, of width $2(d+j_0)$ at the single critical index $j_0$; already collapsed from $\mathrm{\forall }j$ to one inequality by HalfUpperResetCriticalBand.dyadicBandEscape_iff_exists_critical. Only $O(d)$ separation is required here; separation at the square root of the dyadic scale is not needed.

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 $s\ge 5$: a middle (M) branch forces $s+1\le \mathrm{rem}(s+1)$, using no lower bound on the source remainder; with the row-scale source bound this upgrades to $2^{s+1}+(s+1)\le \mathrm{rem}(s+1)$. A minimal-counterexample argument in the same Lean source then shows that any row whose remainder is smaller than its index must have an upper-reset (U) ancestor, since M-ancestors and R-runs are both excluded. Scope of the hypothesis. Two of the three ancestor channels (M, R) are closed unconditionally at all scales; only the U channel remains, and it needs only the $O(d)$-wide band escape of the preceding observation. The 257-reset statement demands escape at the square root of the dyadic scale, whereas linear-width escape at U-resets alone suffices for this argument. Missing step. The single remaining channel: for every $d\ge 13$ with successor carries, the reset charge avoids the width-$2(d+j_0)$ band at its critical dyadic index. Then the remainder is at least the row index at every late middle row, which is the hypothesis of the next observation, and hence $1/2\in \mathcal{A}$; each of these implications is already proved in Lean.

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 ($s\ge 13$, no carry, middle branch) $s\le \mathrm{rem}(s)$, then $1/2\in \mathcal{A}$. The hypothesis is much weaker than an exponential bound, but stronger than the square-root-scale carry bound. Scope of the hypothesis. This hypothesis asks for a linear-in-row lower bound on the remainder itself; the obligation supplies an exponential lower bound on the deviation from $2^s$ at reset rows. For unrestricted numerical values, a large absolute deviation from $2^s$ permits $\mathrm{rem}(s)=0$, which violates the linear lower bound. That observation is not a counterexample within the actual recurrence, so incomparability of the two orbit hypotheses is not established. Missing step. $\mathrm{\forall }s\ge 13$ at a middle transition, $s\le \mathrm{rem}(s)$. The upper-reset band condition described above is one sufficient input to this linear bound; no converse is asserted.

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 $s$ the producer carry exceeds $2\sqrt{2s+2}+4$, then $1/2\in \mathcal{A}$; the producer carry equals the middle coordinate $4\mathrm{rem}-\mathrm{belowPulse}-4$ (Lean source), so the requirement is essentially $\mathrm{rem}(s)\gtrsim (\sqrt{s}+\mathrm{belowPulse})/4$. Comparison. This is a square root of the row index $s$ (a tail majorant for the divisor counts), not the square root of the dyadic scale $2^{(r+5)/2}$. The two square roots in this record are exponentially far apart and easy to conflate; this hypothesis is a bound in the row index. The cited conditional theorem uses it to rule out a last non-right transition. An implication between the different orbit hypotheses would require a further argument. Missing step. $\mathrm{\forall }s\ge 13$ at a middle transition, $4\mathrm{rem}(s)-\mathrm{belowPulse}(s)-4>2\sqrt{2s+2}+4$; a row-scale, not dyadic-scale, lower bound on the middle coordinate.

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 $D\ge 13$, the upper case is excluded. In the middle case put

The cited bounds give $2\le X_{D+1}<2\sqrt{2D+2}+8$. This permits nonnegative $C_D$ as well as the negative exceptional values $-2,-1$; the latter do not exhaust the remaining interval. Scope of the hypothesis. the residual bad set is an explicit $O(\sqrt{D})$-wide integer window at each candidate last non-right transition row, not an interval at dyadic scale. The reset hypothesis would exclude this window. Its width is much smaller than $2^{(r+5)/2}$, but width alone does not measure the difficulty of proving that the actual sequence avoids it. Missing step. Exclude every integer

at a hypothetical last middle transition $D\ge 13$. The ceiling is necessary when converting the strict real upper bound to an integer interval. Excluding only $C_D=-2,-1$ does not suffice.

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 $-3,-2,-1$ is required only on middle branches; the overshoot inequality is required only on right branches where $o_s\le 2^s$. The resulting invariant bounds at least one of the two distances from the target, not necessarily the lower remainder. The exclusion of $-3$ in the special last-middle-then-all-right configuration does not establish the unrestricted middle-branch hypothesis. Both universal assumptions remain to be proved for the actual sequence.

Observation 9.15 (An upper bound on the remainder). SeamGreedyRemainderGapBound, half_mem_mersenneAchievementSet_of_seamRemainderGapBound and the cofinal implication Lean source. The estimate $\mathrm{rem}(s)<2^{s+1}$ for every $s\ge 6$ would give $\mathrm{rem}(s)/4^s\to 0$ and hence $1/2\in \mathcal{A}$. Theorem 6.2 identifies the normalized limit unconditionally; requiring its value to be zero, even only along one unbounded sequence, is equivalent to membership. No strict separation of these conditions on the actual sequence is proved. The upper estimate is also the missing ceiling in the excess-side right-run argument. The existing bound on rows satisfying $2s<3d$, where $d$ is the largest omitted rank, still requires that row condition wherever it is applied. The finite checks do not supply it at every later row.

Observation 9.16 (Reported computation through row 200,000). Conclusion. Exact integer arithmetic to row 200,000 (saved run); branch counts $R:M:U=100197:49899:49898$; within the tested range $6\le r\le \mathrm{200,000}$ the obligation fails only at $r=7$; maximum R-run $19$ after the reset at row $\mathrm{158,096}$ against the required threshold $\approx (r-3)/2\approx \mathrm{79,000}$ (margin $\sim 4000\times$). Independently: 1209 resets checked to row 2500 (saved run), zero classification anomalies, exactly two crossing cells in rows $6\le s\le 2500$ ($s=7,d=5$ and $s=10,d=7$), both below hypothesis scope. Parameter range. fixed-scale exhaustive verification versus a statement at every reset $r\ge 31$. This is the difference between a finite and an unbounded parameter range: a finite verified list supplies no witnesses at unbounded depths, however large the margin. Missing step. The computation records the tested range and its exception at $r=7$; it does not determine a valid threshold for the infinite orbit. A theorem must still establish the proposed bound at every reset beyond its stated threshold.

Observation 9.17 (Structure of resets after long runs). Conclusion. At a dangerous reset $r$ ($|\mathrm{rem}(r+1)-2^{r+1}|\le 2^{(r+5)/2}$) whose preceding reset $r_0$ has pure R-run length $L^{\prime }=r-r_0-1>(r+5)/4$, the deviation $w_{r_0+1}$ is pinned to at most two adjacent integers determined by the divisor-pulse stream alone; a chain of $n$ dangerous resets forces $n-1$ nested exact integer-coincidence towers. Scope of the hypothesis. applies only to dangerous resets preceded by a long pure R-run ($L^{\prime }>(r+5)/4$); an isolated dangerous reset after a short run is untouched. Pinning to two integers is not yet a contradiction: no theorem excludes those two values. This is an ordinary argument; it is not formalised. Missing step. (i) a congruence or pulse-stream obstruction showing the two pinned integer values are unattainable, and (ii) removal of the long-preceding-run hypothesis, or a proof that dangerous resets must enter chains to which the exclusion applies. Excluding the two pinned values addresses only resets satisfying the long-run hypothesis; covering all remaining resets is a separate requirement. Neither step alone proves a global exclusion.

Observation 9.18 (The sign condition and growth of the margin). Conclusion. At all 1209 observed resets, M $\Rightarrow$ deviation $>0$ and U $\Rightarrow$ deviation $<0$, with zero exceptions; the margin over the $2^{(r+5)/2}$ threshold grows from 1.11 bits at $r=14$ to $\sim$1246 bits at $r=2499$. The record isolates this as a separate, possibly more tractable target than the full square-root escape. Different restrictions. The upper sign follows from the positive reset charge: $w_{r+1}=-(4o_r+p_r^{+})<0$. The middle sign is equivalent to $4\mathrm{rem}(r)>p_r$ and needs further information about the orbit. Neither sign implies a square-root lower bound on the absolute deviation. Missing step. Prove that middle inequality and then a quantitative margin on each branch. The exact branch calculation is given in Section 11.1; it is not a substitute for the magnitude estimate.

Observation 9.19 (Comparison of finite truncation lengths). The exact finite procedure in Theorem 8.9 verifies the twenty truncations $3\le J\le 22$. The proof combines finite integer certificates with a witness bound valid beyond the finite search horizon; it does not infer an infinite statement from a long finite run. Saved runs for $3\le J\le 16$ and $17\le J\le 22$ reproduce it. Representations for an unbounded sequence of $J$ would yield a representation of $1/2$ for the full weights by the compactness estimate following that theorem. That unbounded-index premise remains unproved. The size of the least-common-multiple horizon affects this finite algorithm, but is not an impossibility theorem for other arguments.