Reciprocal Mersenne Subseries

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 $C_A(N)\le 2\sqrt{N}+4$ for every $N$. For the greedy support $A=G$ of $1/2$ specifically, this bound is logically equivalent to the theorem’s own conclusion $X_A(2)=1/2$, not a strictly weaker sufficient condition. This follows from the exact residual identity of Lemma 2.4, the unconditional square-root tail bound (binaryCoeffTail_supportCoeff_le_two_sqrt_add_four), the unconditional tail-nonnegativity lemma (binaryCoeffTail_nonneg), and the greedy-specific fact $X_A(2)\le 1/2$. The scope limit is exact: this equivalence does not extend to every $A$ with $1\notin A$; dropping the greedy-specific fact yields only that the bound is equivalent to $\delta \le 0$ (a one-sided condition), not to $\delta =0$. For the related hypothesis 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 $1/2\in \mathcal{A}$ after restricting cofinal witness depths to perfect squares and using the recorded tail bound. The square-root conversion raises no further issue; the open content is the hypothesis itself.

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 $1/2$ skips infinitely many ranks, which is equivalent to $1/2\in \mathcal{A}$ (Lean source). A proof or disproof of this statement settles the half-target question, and conversely; it is not an intermediate step toward it.

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 $G$, not every support omitting $1$. The cofinal terminal condition already works with the original constant $4$, because perfect-square depths avoid a rounding loss. The positive-skip equivalence is stated here at the target $1/2$; extending it to another target requires checking the target-dependent arguments. None of these qualifications supplies the still-missing unbounded sequence of witnesses.