Reciprocal Mersenne Subseries

Observation 9.20 (Exact rows from a sharp capacity bound). exists_exactRowStrictUpperFill_of_skippedCoreSharpCapacity, exactLocalMersenneHalfRow_two_mul_sub_two_of_skippedCoreSharpCapacity. Conclusion. For any $c\ge 4$ and any finite $D\subseteq [2,c)$ with $VD<1/2$ and $SD1(2c-2)<2^{c-2}$: an exact row $E$ at endpoint $2c-2$ with $D\subseteq E$, every new rank strictly above $c$. No additional crossing condition or identification with a greedy prefix is needed. Scope of the hypothesis. needs a per-$c$ input $SD1(2c-2)<2^{c-2}$, and this record supplies that input only through the crossing-deficit route, which eq_halfGreedyPrefixSupport_of_critical_crossing then identifies the core with $D=\mathrm{halfGreedyPrefixSupport}(c-1)$, under its critical-crossing premises. The fill implication does not require that identification; this difference in its formulation is not a proof of strictness between the associated cofinal existence statements. Closes it ($\star$): $\mathrm{\forall }N\mathrm{\exists }c\ge N,\mathrm{\exists }$ finite $D\subseteq [2,c)$ with $VD<1/2$ and $SD1(2c-2)<2^{c-2}$; equivalently $C\uparrow D(2c-3)<2^{c-2}$. No coherence between the $D$’s, no requirement that $D$ be a greedy prefix.

Observation 9.21 (A conditional induction for unbounded depths). SkippedCoreCriticalQuotientSupply $\to$ exists_laterProtectedExactLocalMersenneRow $\to$ 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 $1/2$, or extended using its first crossing rank $e$. In the latter case protection gives $2e-2$ strictly larger than the old endpoint. Scope of the hypothesis. The recycle branch uses the critical quotient supply hypothesis whenever recycling is required. Protection (endpoint $<2\cdot$cutoff and new ranks $>$cutoff) makes that extension strictly increase the endpoint. The induction establishes the conditional implication, not the supply hypothesis. Missing step. The sharp inequality at one crossing rank per step, canonical form HalfGreedySkippedCriticalQuotientSupply: $\mathrm{\forall }c\ge 4$ skipped by the rational half-greedy orbit, $2^{(2c-2)-1}\le Q(\mathrm{insert}c(\mathrm{halfGreedyPrefixSupport}(c-1)))(2c-2)$.

Observation 9.22 (Unconditional capacity, off by one bit). localBinarySuffix_two_mul_sub_two_lt_upperHalfCapacity. Conclusion. Unconditionally, $\mathrm{\forall }c\ge 4$ and every below-half core $D\subseteq [2,c)$ with deficit $<wc$: $SD1(2c-2)<2^{c-1}$. Uniform in $c$, no table, no case split. Parameter range. One bit short. The strict-upper fill needs $<2^{c-2}$, this gives $<2^{c-1}$. The proof derives $A<2^{c-2}+|D|$ then discards $|D|\le c-2\le 2^{c-2}$; the loss is purely additive. The true unproved statement is only that $A$ avoids the linear-width band $[2^{c-2},2^{c-2}+c-3]$, width $c-2$ inside a range of size $2^{c-2}$. Missing step. A linear-width dyadic-band anti-concentration: at cofinally many crossing ranks $c$, $SD1(2c-2)\notin [2^{c-2},2^{c-2}+c-3]$. Same band shape as the earlier linear-band conditions. The reset condition uses a different coordinate and parameter, with width $2^{(r+5)/2}$; no implication between the hypotheses follows merely from this comparison of widths.

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. $\mathrm{\forall }n\ge 6$: a below-half exact row at $n$ produces an exact row at $2n-1$, support-extending, all new ranks $>n$. This is the only unconditional endpoint-doubling step in this record. Scope of the hypothesis. Below-halfness is not preserved and demonstrably fails at the first step. For the seed $D=\{2,3,6\}$ at $M=11$ the core alone contributes $2/3+4/7+32/63\approx 1.746>1$, so the doubled row is strictly above half. Iterating the cheap arm is therefore impossible from the only recorded seed; the chain is forced into the capacity-gated recycle arm at step one. Missing step. Cofinally many below-half exact rows; $\mathrm{\forall }N\mathrm{\exists }n\ge N\mathrm{\exists }D$ exact at $n$ with $\sum _{d\in D}{2}^{nmodd}/(2^d-1)<1$. A single such row at each of cofinally many $n$ makes doubling unnecessary; a self-reproducing one closes everything.

Observation 9.24 (Consecutive-skip precritical bound). halfGreedy_precriticalSuffix_lt_of_next_skip (used in halfGreedySkippedCriticalQuotientSupply_of_precriticalSuffix). Conclusion. Unconditional: if $c\ge 6$ and both rank $c$ and rank $c+1$ are skipped by the rational half-greedy orbit, then $S(\mathrm{halfGreedyPrefixSupport}(c-1))1(2c-3)<2^{c-3}$, doubling into sharp capacity at $c$, hence an exact row at $2c-2$, with no supply hypothesis. Scope of the hypothesis. It needs two consecutive skipped ranks. The residual open set is exactly the skip-then-take rows: halfGreedySkippedPrecriticalSuffixSupply_iff_preTake proves the whole hypothesis equivalent to HalfGreedyPreTakePrecriticalSuffixSupply, with $c=4,5$ already settled by direct computation. Missing step. Cofinally many $c\ge 6$ at which two consecutive ranks $c,c+1$ are both skipped by the rational half-greedy orbit; or dually, the pre-take residual at cofinally many skipped-then-taken ranks. Either one closes the obligation with no further input.

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 $c$, takes at $c+1,\dots ,c+t-1$, skip at $c+t$, with $0<t\le c-3$ and $c-2\le 2^{c-t-3}$ $\Rightarrow$ precritical suffix bound at $c$ $\Rightarrow$ sharp capacity $\Rightarrow$ exact row at $2c-2$. Handles any skip gap $t\lesssim c-3-{\log }_2(c-2)$, not just $t=1$. Scope of the hypothesis. The only missing input is an orbit-level skip-gap bound: that the next skipped rank after $c$ occurs at $c+t$ with $c-2\le 2^{c-t-3}$. The proof is fully uniform in $(c,t)$, every constant explicit, no table. Missing step. For cofinally many skipped ranks $c$ of the rational half-greedy orbit, the next skipped rank is at most $c+(c-3-\lceil {\log }_2(c-2)\rceil )$. The finite skip-density observation does not imply this pointwise gap bound at unbounded ranks. Establishing the latter would supply the hypothesis of the stated conditional argument.

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 $k>0$, $FkJ\ge 0$ for some horizon $J$; the finite coefficient window eventually covers the centred carry. Nonnegativity is monotone up in $J$. Parameter range. For a fixed prefix with positive safety margin, the displayed tail estimate gives a computable sufficient horizon: increase $J$ until $(k+J+3)2^{-J}$ is smaller than that margin. What is not proved is success by the prescribed horizon needed by the exact-row construction. The exact-row route needs the crossing by the specific horizon $J=c-3$ (halfGreedy_precriticalSuffix_lt_iff_frozenMargin_nonneg, $k=c-1$). The quantitative ingredients are already available: binaryCoeffTail_eq_finiteCoeffWindow_add_shiftedTail gives $\mathrm{gap}=\mathrm{tail}(k+1+J)/2^J$, and binaryCoeffTail_le gives $\mathrm{tail}(m)\le m+2$. Available bound. Margin$(k,J)\ge 0$ as soon as $(k+J+3)/2^J<|\mathrm{halfGreedyNextDyadicExcessNumerator}k|/\mathrm{halfGreedyPrefixDenominator}k$. Missing step. At the prescribed horizon $J=k-2$, the displayed bound would suffice if one proved $|E_k|/D_k>(2k+1)/2^{k-2}$ at every skipped rank. The tail estimate uses only lemmas already proved; this stronger margin bound is not established.

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 $n\ge 3$ satisfy $0\le F(n-1)n$. Assuming this property, a Lean theorem proves $1/2\in \mathcal{A}$. Order of quantifiers. The horizon is exactly three doubling steps short. The exact-row hypothesis needs margin$(k,k-2)\ge 0$; this gives margin$(k,k+1)\ge 0$. By the succ-recurrence, margin$(k,k+1)=8\cdot$margin$(k,k-2)+4\mathrm{sc}(2k)+2\mathrm{sc}(2k+1)+\mathrm{sc}(2k+2)$, where $\mathrm{sc}$ is the divisor count, bounded by $\tau \le 2\sqrt{2k+2}$. Since nonnegativity is monotone up in $J$, the cited statement is the weaker one and cannot supply the obligation as it stands. Missing step. A horizon-tightening; at every skipped rank, margin$(k,k+1)\ge 4\mathrm{sc}(2k)+2\mathrm{sc}(2k+1)+\mathrm{sc}(2k+2)$: the full-shell margin must exceed an explicit $O(\sqrt{k})$ divisor-count quantity, on the same square-root scale as the carry bounds above.

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 $\Rightarrow$ the existence of exact quotient sums at unbounded depths $\Rightarrow 1/2\in \mathcal{A}$. Scope of the hypothesis. It is equivalent to the problem itself. The positivity conjunct $0<r(1/2)(c-1)$ holds unconditionally by the odd-denominator parity fact, so the hypothesis says exactly that the greedy rule for $1/2$ skips infinitely many ranks, which Theorem 6.88 proves equivalent to $1/2\in \mathcal{A}$. Thus proving this hypothesis would settle the half-target question itself. What remains. One must prove that this fixed greedy sequence has infinitely many skips. Equivalence neither supplies that proof nor rules out finding a useful invariant for the sequence. The condition in Theorem 6.75 instead permits finite supports that are not greedy prefixes.

Observation 9.29 (Terminal bounds and restrictions on finite support). HalfCarryCofinalTerminalOnlyStrip, HalfTerminalOnlyStripWitness, exists_infinite_support_half_of_cofinalTerminalOnlyStrip. Conclusion. Cofinally many depths $M$ carrying a finite normalized word $a$ with $|\mathrm{ihc}(\mathrm{supp}a)(M-1)|\le BM\Rightarrow \mathrm{\exists }A$ infinite with $X_A(2)=1/2$. Same architecture as the obligation: cofinal, no coherence, mutually incompatible witnesses allowed.

Different restrictions. The terminal condition permits any support inside the depth-$M$ window but demands the carry inside a $\sim 2\sqrt{M}$ strip; the obligation form ($\star$) tolerates a carry up to $2^{M/2-1}$, exponentially looser, but demands the support be confined to ranks $<M/2+1$, since the exact fill encodes the residue in the pure upper window where the Mersenne quotient is exactly $2^{M-d}$. The essential difference is where the support may sit.

Missing step. Confinement of the strip witnesses to the lower half: $\mathrm{\forall }N\mathrm{\exists }c\ge N$ with a strip-scale witness whose support lies in $[2,c)$ at depth $2c-3$. Then $2\sqrt{2c}+4<2^{c-2}$ for $c\ge 8$ gives the required numerical capacity bound. The confinement of the support remains an additional, unproved condition; the comparison does not establish a simpler existence theorem.

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 $2\sqrt{N}+4$ bound on the Möbius-centred carry (Theorem 6.84), each give an infinite support with value exactly $1/2$. Comparison. These bound the carry of the infinite greedy support $G$ of $1/2$; sharp capacity is about the frozen finite prefix $\mathrm{halfGreedyPrefixSupport}(c-1)$. The two carries agree only at index $k$ (inside greedyHalfFrozenMargin_eq_actual_skip_margin), not at depth $2c-3$ where the fill needs it. The bridge is already recorded: halfGreedy_precriticalSuffix_lt_iff_futureSkipCoverage: sharp capacity $\iff CG(2c-4)\le {\mathrm{\Phi }}_c$, where ${\mathrm{\Phi }}_c=\sum _{i=1}^{c-3}{2}^{c-3-i}\mathbf{1}[c+i\notin G]$ is the future-skip capacity; transport costs exactly this term. Missing step. Either a strip bound stated for the frozen prefix rather than the live orbit, or ${\mathrm{\Phi }}_c\ge B(2c-3)$; holds as soon as one skip occurs early in $[c+1,2c-4]$, since the capacity is dyadically weighted. Same input as the bounded-gap precritical bound above.

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 $n$ recycles through its first crossing rank $c$ into a genuine exact row at endpoint $2c-2$, with $4\le c\le n$. No capacity hypothesis at all. Order of quantifiers. The witness is $\mathrm{\exists }c\le n$, not $\mathrm{\exists }c$ large; $2c-2$ may be $\le n$, so the endpoint need not grow. The countermodel of Theorem 6.127 (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 $c>$cutoff, hence $2c-2>$ endpoint; and maintaining those invariants is precisely what needs the sharp-capacity fill rather than this general recycling. Missing step. A crossing-location lower bound; for the supports actually produced, the first crossing rank satisfies $2c-2>n$. Equivalently, keep protection alive without sharp capacity, e.g. a fill placing all new ranks above $c$ using only the recorded $c-1$-bit capacity.

Observation 9.32 (Double-or-recycle dichotomy, proved insufficient). exactLocalMersenneHalfRow_double_or_recycle, boundedDoubleOrRecycleModel_not_cofinal, exists_seeded_bounded_double_or_recycle_model. Conclusion. $\mathrm{\forall }n\ge 6$, an exact row at $n$ gives an exact row at $2n-1$ or at $2c-2$ for some $4\le c\le n$; plus a formal proof that this shape, even seeded at endpoint six, is logically insufficient for cofinality. Order of quantifiers. The dichotomy is proved by splitting on the sign of the witness value (odd denominators exclude equality); the countermodel pins the deficit precisely: what is missing is not another dichotomy but strict endpoint progress in the recycle branch, or a proof that the below-half branch recurs. Re-deriving this dichotomy without controlling repeated returns to bounded depths would leave the same gap. Missing step. Either (a) the recycle branch upgraded to $2c-2>n$, or (b) cofinally many below-half exact rows so the doubling branch alone is cofinal. These are two sufficient ways to obtain progress; the countermodel does not rule out other assumptions that also force unbounded depths.