Reciprocal Mersenne Subseries

Observation 9.33 (A sufficient block-certificate condition). irrational_erdosSupportSeries_of_weighted_coeff_certificates (carry variant Lean source). Conclusion. $\mathrm{\forall }b\ge 2,\mathrm{\forall }A\subseteq \mathbb{N}$ (no infinitude, no structure hypothesis at all): if $\mathrm{\forall }q>0\mathrm{\exists }N,K,L,C$ with $K\le L$, $b^r\mid c_A(N+r)$ for $r\in [1,K]$, $\sum _{r=K+1}^L{c}_A(N+r)b^{L-r}\le C$, $\mathrm{\exists }t,0<c_A(N+L+1+t)$, and $q(C+N+L+2)<b^L$, then $X_A(b)$ is irrational. The cited full-support, multiples, periodic, residue-class, pairwise-coprime and fixed-core constructions use this criterion. No such factorisation is asserted for the weighted support theorem in Section 1. Scope of the hypothesis. The criterion is already universally quantified over $A$; the universal quantifier is not the gap. The certificate hypothesis must hold at every precision, and it is supplied only for named classes; certificate existence for an arbitrary infinite $A$ remains open. Limit of this sufficient condition. Supplying these certificates for every infinite support would imply the universal statement, but Proposition 11.4 rules out that supply for the two specified certificate schemes. The carry variant replaces digit-wise divisibility by aggregate divisibility $b^K\mid \sum _r{c}_A(N+r)b^{K-r}$; the squarefree obstruction applies to that variant too. Universal certificate supply is therefore not being posed as an unresolved equivalent formulation of Problem 257.

Observation 9.34 (Rational targets and infinitely many greedy skips). half_mem_mersenneAchievementSet_iff_greedySkippedSupport_infinite (forward Lean source; reverse mem_mersenneAchievementSet_of_greedySkippedSupport_infinite). For every rational $x\ge 0$,

The reverse implication holds for every real $x\ge 0$: a fatal remainder $r_n(x)>R_n$ forces every subsequent weight to be taken, because $R_n=w_{n+1}+R_{n+1}$. Hence infinitely many skips exclude a fatal remainder, and Theorem 1.11 gives membership. For the forward implication, membership identifies the greedy sum with $x$. Finitely many skips would make that sum $E$ minus a finite rational sum, which is irrational by Erdős’s theorem [1]. This contradicts rationality of $x$ and proves the stated extension as an ordinary argument.

Infinitely many skips do not mean infinitely many selected ranks: $x=1/3$ has the single-element support $\{2\}$ and skips every other rank. Thus the equivalence does not decide which rational targets are represented, or provide an infinite support with rational value. The Lean declarations above concern the half target; the extension to every rational target is an ordinary argument and is not formalised.

Observation 9.35 (Finite sums exclude every rational with even denominator). finite_boolSupport_ne_half; the underlying parity lemma has its own finiteErdosSum_den_odd. Conclusion. $\mathrm{\forall }A$ finite with $0\notin A$: $X_A(2)\ne 1/2$; any support achieving exactly $1/2$ must be infinite. Parameter range. The statement is specific to the target $1/2$, while the underlying parity lemma (the reduced denominator of a finite sum is odd) holds for every finite support. The same argument in general. For every rational $t$ with even reduced denominator and every finite $A$ with $0\notin A$, $X_A(2)\ne t$; the proof is the same. Thus a represented rational with even reduced denominator would refute universal #257 at $b=2$. The converse is not established. If $\mathcal{F}$ denotes the set of finite-support values, the exact unrestricted condition is $(\mathbb{Q}\cap \mathcal{A})\setminus \mathcal{F}\ne \varnothing$.

Observation 9.36 (The denominator in the reciprocal-mass estimate). dyadic_support_fraction_reciprocalMass_diverges_or_gt_one; the version for general $v$ has its own shiftedBooleanCollision_wrap_bound_of_common_multiple. Conclusion. For $A$ infinite with $X_A(2)=p/2^c$ (dyadic rational): $\sum _{a\in A}1/a$ diverges or exceeds $1$. Comparison. The result is restricted to denominators $2^c$ ($v=1$), while the obligation needs every rational $p/(2^{c}v)$. The restriction is one of application, not of proof: every supporting lemma allows an arbitrary positive $v$, and the general-$v$ conclusion is already recorded for arbitrary $(v,h,L,F)$. Missing step. Instantiate the recorded generic theorem at $F=\{a,b\}$, $L=\mathrm{lcm}ab$, $h=$ multiplicative order of $2$ mod $v$, giving $\rho (A)\ge \mathrm{doublingWrapCount}(p,v,h)/h+1/\mathrm{lcm}(a,b)$ for every rational value. The one genuinely new step: for $v>1$ the excess can be $0$, so strictness needs $1\le \mathrm{doublingWrapCount}(p,v,h)/h+\lfloor |F|/2\rfloor /L$ (equivalently: the mean least residue of $p\cdot 2^{n}modv$ is $\ge v(1-|F|/2L)$).

Observation 9.37 (Zero windows of a fixed support). supportCoeffZeroWindow_length_le_eps_logb. Conclusion. For any $A$ with a positive element and $X_A(2)=p/(2^{c}v)$, $v>0$ (any rational, not just dyadic): for every $\epsilon >0$ there is $B\ge 0$ such that, for all $N\ge 1$, every run of $h$ zero divisor counts starting after $c+N$ has $h\le \epsilon {\log }_{2}N+B$. The constant $B$ may depend on the fixed support and the other parameters. More basically, if $a_0$ is any positive element of $A$, then each block of $a_0$ consecutive integers contains a multiple of $a_0$. Every zero window of $c_A$ therefore has length at most $a_0-1$, whether or not $X_A(2)$ is rational. For a fixed nonempty support, the displayed logarithmic bound thus gives no additional restriction. A proposed alternative between super-logarithmic zero windows and general block certificates cannot split this class: the first branch is already impossible. It would require the certificate branch for every support, which the obstruction in Proposition 11.4 rules out for the specified schemes.

Observation 9.38 (Prime support and the reciprocal-sum hypothesis). irrational_erdosSupportSeries_pairwise_coprime (its certificates: exists_weighted_coeff_certificates_supportCoeff_pairwise_coprime). Conclusion. For every $b\ge 2$, an infinite pairwise-coprime support with summable reciprocal mass has irrational support series. Method boundary: the primes satisfy the other hypotheses but $\sum _{p}1/p$ diverges, so this Lean theorem does not apply. It is false, however, to infer that the base-$2$ prime-support value is open. Tao–Teräväinen prove

irrational in Theorem 1.3 of their 2025 preprint. That result is cited, not formalised here. What remains is a test of the method: replacing the global tail budget by a windowed one would ask whether this particular certificate theorem can recover the known theorem. It is no longer an open mathematical target or a claimed new route for #257.

Observation 9.39 (The two hypotheses of the sunflower criterion). irrational_erdosSupportSeries_of_orthogonalPetalBouquet. Conclusion. For $A=$ (finite exceptional set dividing $Q$) $\cup \{{\mathrm{core}}_i\cdot {\mathrm{petal}}_i\}$ with cores $\mid Q$, petals pairwise coprime and coprime to $Q$, $\sum 1/{\mathrm{petal}}_i<\mathrm{\infty }$: if $A$ satisfies the tail-selection hypothesis below, then its series is irrational.

Different restrictions. Two gaps. (i) On the support: the bouquet class strictly generalises pairwise-coprime supports but still demands globally pairwise-coprime, summable petals; it inherits the exclusion of the primes noted in the preceding observation and adds nothing in the divisor-dense regime. (ii) On the selector: the tail-selection hypothesis must hold at every precision and is unproved.

Missing step. For the selector, $\mathrm{\forall }K>0\mathrm{\exists }N$, $2^K\mid$ the carried first block $\wedge \sum _{j\ge 1}{c}_A(N+K+j)2^{-j}\le 16$, from the bouquet’s persistent-reduced-modulus averaging. For the class: the assertion that every infinite $A$ admits a bouquet structure is false (take $A=$ all multiples of 6: there is no coprime petal decomposition). A theorem for every infinite support would therefore require a different structural hypothesis, not merely a proof of that false existence assertion.

Observation 9.40 (What eventual periodicity supplies). irrational_erdosSupportSeries_eventuallyPeriodic. Conclusion. $\mathrm{\forall }b\ge 2\mathrm{\forall }m>0\mathrm{\forall }{N}_0$: $A$ infinite and $m$-periodic above $N_0$ $\Rightarrow$ irrational. Plus: the class of supports with irrational series is closed under finite symmetric difference in both directions. The statement follows from the periodic theorem of Luca and Tachiya [3].

Scope of the hypothesis. The theorem allows every positive period and every finite starting threshold. It still requires an eventually periodic support, so it does not include all aperiodic supports covered by the other criteria in this record. Finite symmetric difference preserves eventual periodicity. Thus the finite-perturbation argument alone cannot extend this theorem to an aperiodic tail; a further hypothesis or argument is needed.

Missing step. A “locally periodic at cofinally many scales” version; $\mathrm{\forall }q>0\mathrm{\exists }N\mathrm{\exists }m\le f(N)$ such that $A\cap [N,N+L]$ is $m$-periodic for $L$ large enough that the periodic sieve manufactures one block certificate. The periodic argument already needs periodicity only across the certificate window, so this is the closest genuine widening; but proving that periodic windows exist at unboundedly many scales for arbitrary $A$ is a new statement.

Observation 9.41 (The reduced denominator in a gap criterion). irrational_erdosSum_of_lcm_gap (instances irrational_erdosSum_factorial_support, irrational_erdosSum_two_pow_support). Let $A=\{a_0<a_1<\cdots \}\subseteq {\mathbb{N}}_{>0}$, let $b\ge 2$ be an integer, and write the first $k$ terms in lowest terms as

A sufficient irrationality condition is

The next omitted exponent is $a_k$, not the last exponent included in $S_k$. Since $a_{k+j}\ge a_k+j$, the positive omitted tail obeys

If $X_A(b)=p/q$ were rational, positivity would give $q{Q}_k(X_A(b)-S_k)\ge 1$. The displayed tail estimate contradicts this under the proposed condition. This is the denominator-times-error argument in irrational_of_den_mul_abs_sub_tendsto_zero, with all indices specified.

For $L_k=\mathrm{lcm}(a_0,\dots ,a_{k-1})$ one has $Q_k\mid b^{L_k}-1$, hence ${\log }_b{Q}_k<L_k$. Thus the earlier condition $a_k-L_k\to \mathrm{\infty }$ suffices. Using actual reduced denominators can improve this estimate, but requires an upper bound for $Q_k$ relative to $b^{a_k}$. A surviving-divisor lower bound does not provide that upper bound. In particular, the divisibility statement in Lean source and the lower bound in upperHalfMersenneProduct_lower_bound do not alone establish the proposed condition for an arbitrary support. No such condition is proved here for the remaining dense supports.

Observation 9.42 (Rationality expressed by the integer carry). erdosSupportSeries_rational_iff_exists_temperedCarry; the general criterion of Theorem 6.105 has its own binaryCoeffSeries_rational_iff_exists_temperedBinaryOrbit. Conclusion. For every $A\subseteq \mathbb{N}$, with no hypothesis: $X_A(2)$ is rational if and only if there are $q>0$ and $U:\mathbb{N}\to \mathbb{Z}$ with $U(N+1)=2U(N)-q{c}_A(N+1)$ and $U(N)/2^N\to 0$. Comparison. This is already universal over $A$; it is the exact form in which the obligation should be stated, and the argument literally shared with #249 (take $c=\phi$ in Theorem 6.105). It does not refute the orbit: temperedBinaryOrbit_eq_scaledTail pins the orbit uniquely to $u(N)=q{T}_c(N)$, and $T_c(N)\le N+2$ confirms it is never ruled out on growth grounds for any $c$ with $c(n)\le n$. Missing step. A support-specific non-existence theorem: for every infinite $A$ and every $q>0$, no such $U$ exists. Because the criterion is an equivalence and the orbit is unique, this is logically equivalent to the obligation; its value is to name the single object (the tempered carry orbit of $c_A$) whose non-existence is the entire content, for every $A$ at once.

Observation 9.43 (Why unbounded carry alone is insufficient). shifted_state_unbounded_of_infinite_support, exists_unbounded_shifted_odd_tail_nat_state_of_support_fraction, one_add_mul_card_le_two_mul_shifted_state. Let $A\subseteq {\mathbb{N}}_{>0}$ be infinite, let $c\ge 0$ and $v\ge 1$ be integers, and let $u(n)$ be positive integers satisfying

For a finite $F\subseteq A$ and a common multiple $L$ of its elements with $L>c$, put $n=L-c-1\ge 0$. Directly from the recurrence,

This argument uses positivity of the next state, not an assumed tail representation or a limit condition. A general positive solution may also have an exponentially growing homogeneous part. The condition $L>c$ ensures that the coefficient row really is $L$; truncated natural-number subtraction cannot replace it.

Finite subsets $F$ of arbitrarily large size, followed by positive common multiples exceeding $c$, prove that $u$ is unbounded. In the tempered case the separate identity $u(n)=v\sum _{r\ge 1}{c}_A(c+n+r)2^{-r}$ gives $u(n)\le v(c+n+2)$. Unboundedness is consistent with this linear upper bound and with $u(n)/2^n\to 0$. A contradiction would require an incompatible upper estimate at the same chosen indices.

Observation 9.44 (A finite-gap criterion for every target in the convex hull). half_mem_mersenneAchievementSet_or_exists_fatal_gap, half_mem_mersenneAchievementSet_iff_no_existsFatalHalfGap; the exclusion for a general support has its own positiveMersenneSupportValue_ne_of_rank_gap. For every real $x\in [0,E]$, not just rational targets, one has

Here $R_m=\sum _{j>m}{w}_j$. The implication to the right has a short greedy proof. If $x\notin \mathcal{A}$, choose the first $m$ with $r_m(x)>R_m$ using Theorem 1.11. Since $r_0(x)=x\le E$, we have $m\ge 1$ and $r_{m-1}(x)\le R_{m-1}=w_m+R_m$. A take at $m$ would leave a remainder at most $R_m$, so this step must be a skip. Thus $R_m<r_{m-1}(x)<w_m$, giving the displayed gap with the greedy prefix $D$.

Conversely, the displayed gap contains no achievable value. A support with prefix $D$ either skips $m$, giving value at most $X_D(2)+R_m$, or takes $m$, giving value at least $X_D(2)+w_m$. A different prefix first differs at some $j<m$; the inequality $w_j>R_j$ orders its entire continuation interval strictly on one side of the interval with prefix $D$. Both gap endpoints themselves are achievable, by the supports $D\cup \{m+1,m+2,\dots \}$ and $D\cup \{m\}$. Consequently no parity argument or irrationality assertion about $E$ is needed for this ordinary general-target dichotomy. The restriction to $[0,E]$ is essential to this formulation: targets outside the convex hull are already excluded and need not lie in an internal gap. The general-target equivalence and both endpoint constructions are Lean-checked in paper_general_target_gap.

Observation 9.45 (Why the signed periodic theorem still requires periodicity). irrational_or_bpow_mul_eq_intCast_intWeightedErdosSeries_periodic, irrational_intWeightedErdosSeries_periodic_of_coeff_nonneg_of_frequently_ne_zero. Conclusion. $\mathrm{\forall }b\ge 2\mathrm{\forall }m>0\mathrm{\forall }$ $\mathbb{Z}$-valued $m$-periodic weight $w$: irrational$(\sum w(a)/(b^a-1))$ $\vee$ $\mathrm{\exists }k,z,b^{k}x=z$; the terminating branch closes unconditionally as soon as $c_w$ is one-signed and frequently nonzero. Luca and Tachiya’s theorem already gives irrationality for every nonzero periodic weight [3].

Different restrictions. Two mismatches. (i) Periodicity of the weight is still required; this is the signed version of the periodic-support theorem and keeps its periodicity hypothesis. (ii) The one-sidedness clause is automatic for #257 (a $0/1$ support indicator gives $c_A\ge 0$), so the sign conditions add nothing here; they were designed for the signed #249 argument. The genuinely transferable content is the dichotomy shape itself: irrational-or-$b$-adically- terminating, terminating branch killable by a positive far tail.

Missing step. An aperiodic version of the dichotomy; for arbitrary $A$, either $X_A(2)$ is irrational or $2^k\cdot$it is an integer. For arbitrary infinite $A$, exclusion of the terminating branch is itself an additional unproved assertion; finite-support odd-denominator parity does not pass automatically to an infinite limit. An aperiodic dichotomy together with a valid terminating-branch exclusion would close the obligation. Periodicity is used only to manufacture the full-block certificates, so removing it again requires the missing supply of certificates for arbitrary supports.