Reciprocal Mersenne Subseries

The statement needed

The exact-row transition exactLocalMersenneHalfRow_double_or_recycle says every exact row $n\ge 6$ either doubles to $2n-1$ or recycles to $2c-2$ for some $4\le c\le n$. Exact rows at unbounded depths, which give $1/2\in \mathcal{A}$, need the recycle branch not to return to a bounded endpoint forever. Three sufficient forms:

where $v(D):=VD$ (SkippedCoreCriticalQuotientSupply);

Unboundedness of $g$ alone would not suffice in (c). For example, $g(n)=\lfloor n/2\rfloor +1$ tends to infinity but allows the fixed transition $n=6$, $c=4$, $2c-2=6$. The displayed strict-progress inequality excludes such cycles; the doubling branch already increases every endpoint $n\ge 6$.

What kind of object would furnish it

The real and integer greedy rules must be distinguished here. A real straddling word agrees with the real greedy prefix (IsStraddlePrefix.half_agrees_greedy). An exact local row instead satisfies $QDn=2^{n-1}-1$. Although floor division is not injective in general, the quotient weights at fixed $n$ have a gap of at least $1$ between distinct subset sums. A witness is therefore unique when it exists and is recovered by the integer greedy test (Theorem 6.100 and Propositions 6.101–6.102). There is no exponential family of witnesses to choose from at that depth. What remains to prove is that successful depths are unbounded.

One possible additional ingredient is an integer-valued function $\mathrm{\Phi }(n,D)\ge 0$ on reachable exact rows that increases by at least one under each permitted transition and is bounded on rows of bounded endpoint. Along an infinite trajectory, $\mathrm{\Phi }$ would then tend to infinity, forcing the endpoints to be unbounded. Strict increase only on recycle steps would need a separate check of what doubling does to $\mathrm{\Phi }$; an unspecified real-valued increasing quantity need not tend to infinity. This describes one possible proof mechanism, not a necessary class of all proofs. The record already has the sharp capacity test in exact form: by localBinarySuffix_two_mul_sub_two_lt_criticalCapacity_iff, form (a) is exactly the statement that the $c-2$-bit suffix capacity $SD1(2c-2)<2^{c-2}$ is met.

The specific obstacle

The formal counterexample concerns exactly the transition schema: that schema plus a seed provably does not give cofinality. The theorem exists_seeded_bounded_double_or_recycle_model exhibits the one-point predicate $P(n):=(n=6)$, which satisfies the seed (exactLocalMersenneHalfRow_six, the explicit witness $\{2,3,6\}$) and the exact shape of the transition, and is not cofinal. So no argument that uses only the dichotomy and the base case can work, however cleverly the induction is arranged. Any proof must use arithmetic content of exact rows that the abstract schema does not see.

There is a second, more specific trap, and it is also formalised. The natural sufficient condition via fractional split mass is not necessary: the example at $D=\{2,3\}$, $c=5$ (splitFractionMass_one_bound_not_necessary_fixture) exhibits a real crossing core violating it. Thus the fractional-mass bound is not necessary for an individual crossing core. This counterexample does not rule out proving that sufficient bound on a more restricted family.

Possible estimates to prove

The uniquely determined prefix at a crossing. The identification below is proved; the required capacity bound remains open.

Form (a) is universally quantified over cores $D$, which looks like an exponential obligation. It is not. Its hypotheses are exactly those of eq_halfGreedyPrefixSupport_of_critical_crossing, which forces $D=G\cap \{1,\dots ,c-1\}$. So the $\mathrm{\forall }D$ collapses to a single orbit and form (a) is a statement to be checked along one sequence indexed by $c$, namely

The crossing hypothesis has not disappeared: these are the ranks where the real greedy rule skips the next term. Each resulting finite inequality is decidable. Computing its margin can identify examples to explain a proposed estimate, but a finite table neither selects a proof method nor establishes a cofinal supply.

The progress-function criterion above remains unproved. Endpoint doubling is not a proved doubling law for the largest selected exponent, and an unbounded function of the incoming endpoint alone does not rule out a bounded cycle.