Apply a result and change a hypothesis

Does the weighted #257 result apply when a hypothesis changes?

Source fingerprint: f2e067e7a9f5a4ad (authored regions, claim, boundary, paper and Lean sources).

Read this saved file offline, with or without an assistant. No clone, account or Lean installation is needed. Links identify the public sources when you are online.

Your task: decide what the weighted criterion says for the three cases below. Ask for one hint, a second hint, or the worked answer; an assistant should stop at your chosen depth. Collapsed answers are present in this file for offline reading.

Case	Changed hypothesis
1	$c=2,p=1,b=2$
2	$c=2,p=1,b=3$
3	$c=2,p=2$ : what follows at every integer base $b\ge2$ ?

Criterion and definitions

$X_A(b)=\sum_{a\in A}(b^a-1)^{-1}$ is the support series. $W_{b,P}$ denotes weighted mass, and $v_p(a)$ is the exponent of prime $p$ in $a$ .

For a finite nonempty prime set $P$ , let $h_P(a)=\prod_{p\in P}p^{v_p(a)}$ . If $b\ge2$ , $A$ is an infinite set of positive integers, and

$\sum_{a\in A}\frac{h_P(a)}{a(b^{h_P(a)}-1)}<\infty,$

then $\sum_{a\in A}(b^a-1)^{-1}$ is irrational. Separately, if a host $H$ of positive integers has finite weighted mass at base two for some such $P$ , then every infinite subset $A\subseteq H$ has an irrational support sum at every integer base $b\ge2$ . The paper states both clauses and their hereditary consequences at res:weighted-support in paper/257/erdos-257-mersenne-support-subseries.tex.

Registered claim and source boundary

Claim finite_prime_weighted_support: unconditional progress, projected from docs/claims.json. This status means the criterion is proved with its stated hypotheses; it does not remove those hypotheses.

For every integer base b >= 2, every infinite positive support A with finite weighted mass for some finite nonempty prime set P has irrational support series. If a host H of positive integers has finite base-two weighted mass, then every infinite subset A of H has irrational support series at every integer base b >= 2. This is a sufficient support criterion, not the universal statement.

Open boundary remaining_open.universal_257_all_infinite_supports: open. Prove irrationality for every infinite support A, not only the named support families formalised here.

Exact checked criterion: ErdosProblems.Erdos257.PaperCompleteR8.divisibilityWeightedClaim in lean/ErdosProblems/Erdos257/PaperCompleteR8/WeightedReturn.lean:120. Its conjunction type and weighted definitions are in AnalyticTargets.lean.

Lean proves the conditional criterion. The parameterised family calculation below is an ordinary deduction from the paper’s dyadic estimate, not a separately named Lean-checked instance. Finite samples cannot establish these infinite convergence claims.

Exercise, hints and worked answer

The paper’s example uses the support $A_\star=\{2^km:k\ge1,\ m\text{ odd},\ m\le2^{2^k}\}$ . Its reciprocal sum diverges, yet its base-two weighted mass is finite, so Theorem 1 applies to every infinite subset at every integer base. What changes if the odd-factor cutoff in layer $k$ becomes $2^{r_k}$ , where

$r_k=\left\lceil\frac{c^{2^k}}{k^p}\right\rceil, \qquad c\ge2\text{ an integer},\quad p>0?$

For $c=2,p=1$ , decide whether the $P=\{2\}$ weighted test works at bases $2$ and $3$ . Then change only $p$ to $2$ and decide what Theorem 1 says at every base. Before opening the calculation, distinguish “this test fails” from a claim that the corresponding series is rational.

Show one hint

Write the weighted mass layer by layer using $P=\{2\}$ . Compare the odd harmonic sum with $r_k$ before deciding convergence. Stop here if you want to do the comparison yourself.

Show a second hint

Use $r/4\le S_r\le r$ and compare $(c/b)^{2^k}/k^p$ with the weighted term. At $c=b$ , the exponent cancels and the power $p$ decides the test. A divergent sufficient test does not establish rationality.

Show the calculation and decisions

Put $A(c,p)=\{2^km:k\ge1,\ m\text{ odd},\ 1\le m\le2^{r_k}\}$ and $S_r=\sum_{1\le m\le2^r,\ m\text{ odd}}1/m$ . The dyadic estimate in the paper’s example gives $r/4\le S_r\le r$ for $r\ge1$ . Layers are disjoint because $2^km$ has exactly $k$ factors of $2$ . Hence

$\sum_{a\in A(c,p)}\frac1a=\sum_{k\ge1}\frac{S_{r_k}}{2^k}, \qquad W_{b,\{2\}}(A(c,p))=\sum_{k\ge1}\frac{S_{r_k}}{b^{2^k}-1}.$

The reciprocal sum diverges for every listed $c,p$ : its $k$ th layer is at least $c^{2^k}/(4k^p2^k)$ , which does not tend to zero. For the weighted sum, $r_k$ lies between $c^{2^k}/k^p$ and $c^{2^k}/k^p+1$ . The same bounds on $S_r$ , and $b^{2^k}/2\le b^{2^k}-1\le b^{2^k}$ , bound its $k$ th term below by $(c/b)^{2^k}/(4k^p)$ and above by $2(c/b)^{2^k}/k^p+2b^{-2^k}$ . Therefore:

Changed condition	$P=\{2\}$ weighted test at base $b$
$b>c$	Converges
$b=c$ and $p>1$	Converges
$b=c$ and $0<p\le1$	Diverges
$b<c$	Diverges

For $c=2,p=1$ , the test passes at base $3$ and every larger integer base. The fixed-base clause therefore makes $X_B(b)$ irrational for each such base and every infinite $B\subseteq A(2,1)$ . At base $2$ , this particular test diverges: it gives no arithmetic verdict there. Another witness or argument has not been ruled out. When $p=2$ , the base-two test passes; the all-base clause makes $X_B(b)$ irrational for every integer $b\ge2$ and every infinite $B\subseteq A(2,2)$ .

This parameterised calculation is an ordinary deduction from the paper’s criterion and its dyadic bound. The Lean declarations prove the conditional criterion, not a named theorem about this family. The unrestricted Erdős #257 question remains open.

A useful next question

Can a different fixed finite prime witness decide the case where this test diverges? Return an argument, obstruction, or precise non-answer with its source and assumptions. Failure of this witness does not settle the universal question.

Source content identities

paper/257/erdos-257-mersenne-support-subseries.tex: SHA-256 d72b79f31d5438b24af1f4c73ddc357234412a30f0a8af857e7e5af85acba8b3
lean/ErdosProblems/Erdos257/PaperCompleteR7/AnalyticTargets.lean: SHA-256 7d9cbb3b225cbad70ae1f8165560dc15602525143a64dccf9457259fbbdc9d0a
lean/ErdosProblems/Erdos257/PaperCompleteR8/WeightedReturn.lean: SHA-256 c00b39ee574aaec577de2cbc6971c12ca5865c8891f0c8fa88b9ba63335e92a0

Public paper text · Author-owned exercise · Return or correct work