Reciprocal Mersenne Subseries

The statement needed

The following five conditions are equivalent to $1/2\in \mathcal{A}$:

1. $C_G(N)\le 2\sqrt{N}+4$ for every $N\ge 0$.

2. The set ${\mathbb{N}}_{>0}\setminus G$ is infinite.

3. For arbitrarily large $n$ there is $D\subseteq \{2,\dots ,n\}$ with $Q(D,n)=2^{n-1}-1$.

4. For arbitrarily large $M$, $\mathrm{ihc}(G,M)\le B(M+1)$.

5. For arbitrarily large $M\ge 1$ there is $D\subseteq \{2,\dots ,M\}$ with $|\mathrm{ihc}(D,M-1)|\le B(M)$.

Here $G$ is the actual greedy support for $1/2$. The forward directions of (2)–(5) are proved in Lean (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

The difference between the real and the integer square root disappears when cofinal witness depths are restricted to perfect squares: at $n=k^2$ the two roots coincide exactly and no widening is needed. Applying Lemma 11.3 along $M=k^2-1$ gives (4) directly; taking $a$ to be the indicator of an achieving support truncated to $\{0,\dots ,M\}$ at $M=k^2$, and using integerHalfCarry_inter_Iic_eq_of_succ_le together with $1\notin A$ (forced because $w1=1>1/2$), gives the witness required by 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 $A$ with $1\notin A$: without erdosSupportSeries_greedyMersenneSupport_le (which supplies $\delta :=1/2-S_G\ge 0$ for the greedy support specifically) one obtains only the one-sided equivalence of the bound in (1), with $A$ in place of $G$, and $1/2-S_A\le 0$. The mechanism in all five cases is the same and should be recorded once: $2^{N+1}\delta$ dominates any $\sqrt{N}$ envelope, so a strip hypothesis forces $\delta =0$; and $\delta =0$ makes the unconditional tail bound supply the strip. Membership is then read off by mem_mersenneAchievementSet_iff_greedy_survival.