Reciprocal Mersenne Subseries

Proposition 10.9 (A finite-state restriction for the stated pulse family). For a “balanced pulse” family at location $m\ge 2$ (radius $\rho =\lfloor (m+1)/2\rfloor$, parameters $0\le r\le \rho$, moving mass between positions $m$ and $m+1$ with the weighted total $2c(m)+c(m+1)=2\rho$ of the two coefficients fixed), if a predecessor state is constant across the whole family, then no function $\mathrm{decode}:\mathrm{State}\to \mathbb{N}$ can recover the parameter $r$ from $\mathrm{state}(r)$ for every $r$. The family has exactly $\rho +1=\lfloor (m+1)/2\rfloor +1$ members, so the fan-out is unbounded in $m$. More strongly, any finite set of states carrying an exact decoder for the family has at least $\rho +1$ elements, unbounded in $m$.

Scope. Excludes bounded-state encodings of pre-$m$ history that must distinguish every member of the displayed balanced-pulse family, whether the coefficients are $\phi$ or a Möbius-support indicator. Applying it to #249 or #257 requires showing that the relevant orbit realises that family, and it does not rule out every finite-state proof strategy. Object or representation: about a representation class, the encodings of history that separate the balanced-pulse family; it says nothing about $C$ or $\mathcal{A}$ directly.

Proposition 10.10 (Möbius-support countermodel: the natural negative-sign candidate overshoots). The signed Lambert identity $\sum _{d\ge 1}\mu (d)/(2^d-1)=1/2$ is exact. Writing $N:=\{d:\mu (d)=-1\}$: $\sum _{d\in N}1/(2^d-1)=1/2+\sum _{d\in P}1/(2^d-1)$ where $P:=\{d\ge 2:\mu (d)=1\}$, and quantitatively $1/2+1/63\le \sum _{d\in N}1/(2^d-1)$ (using the first positive tail term $d=6$, $\mu (6)=1$) ; the negative-Möbius support strictly overshoots $1/2$ by at least $1/63$.

Scope. Rules out exactly one natural candidate infinite Boolean support (the negative-Möbius set) as a witness for $1/2\in \mathcal{A}$. A route-sufficiency no-go only ; it says nothing about whether some other infinite Boolean support sums to $1/2$. Object or representation: about the object ; a genuine value inequality for one specific candidate set, not a coordinate artifact. Margin $1/63$ is the concrete number any repair attempt (adding/removing finitely many elements) must close or exceed.

Proposition 10.11 (Finite computation and half-membership). No finite positive-index Boolean support has value exactly $1/2$: the reduced denominator of any finite Mersenne subset-sum is provably odd (each $2^n-1$ is odd), while $1/2$ needs an even denominator. Separately, $\mathsf{CertifiedGreedyMersenneDeath}$ is a finite-depth certificate of $x\notin \mathcal{A}$, obtained by decidable tests on rational input. For example, the supplied source excludes $3/4$ at level $1$ with lookahead $0$. Failure to find such a certificate at a given depth does not establish membership. It records survival of that finite test, not survival at every depth.

Scope. Any support representing $1/2$, if it exists, must be infinite. This follows from denominator parity, independently of the certificate search. The search supplies a different fact: a successful exclusion certificate proves nonmembership, whereas its absence in a bounded search does not prove membership or rationality. The same distinction must be checked separately for any other certificate family.

Proposition 10.12 (Period exclusion for the totient series). For $\sum _n\phi (n)/2^n$, the cited finite test proves that $\mathrm{totientTail}(N+h)-\mathrm{totientTail}(N)$ is not an integer by excluding every possible integer state in a bounded range within finitely many steps. If the series were rational, some positive period $h_0$ would make these tail differences integral for every sufficiently large $N$. Telescoping would then give integrality also for every positive multiple $m{h}_0$.

Consequently, the required certificate supply is: for every $h_0\ge 1$ and every lower bound $N_0$, there exist $m\ge 1$, $N\ge N_0$ and a finite test length $K$ excluding integrality for $(m{h}_0,N)$. The unbounded choice of $N$ is essential; a counterexample before the unknown eventual threshold does not exclude an eventual period. It is sufficient instead to obtain such certificates for $h=\mathrm{lcm}(1,\dots ,t)$ with both $t$ and $N$ exceeding arbitrary prescribed lower bounds. The supplied finite theorem excludes the tail differences for $1\le h\le 16$ at $(N,L)=(14,9)$, and hence excludes rational values whose reduced denominator divides $2^{14}(2^h-1)$ for one of those $h$. It does not establish the unbounded certificate supply.

Scope. The Lean declarations used in this comparison concern the totient series of Problem 249. Their carry recurrences may suggest constructions for Problem 257, but applying them there requires a new argument for the divisor transform of its chosen support. The totient-specific theorems do not supply that argument.