Weighted support theorem for reciprocal Mersenne subseries (Erdős #257)

For every integer base b at least two and every infinite positive-integer host H with a finite nonempty prime set witnessing finite b-weighted mass, the reciprocal Mersenne subseries on every infinite subset A of H is irrational at b. If H instead has such a witness for base two, every infinite subset A has an irrational subseries at every integer base b at least two. The host witness is chosen before the subset and base in the second clause. Taking A = H recovers the two direct assertions of Theorem 1.

Where to inspect the proof. The := by sorry on this page is Prove2Me’s challenge placeholder, not the accepted proof. The accepted Solution is stored separately under View graph → Solutions & Sketches; the graph route currently asks signed-out readers to sign in. The public proof packet prints the byte-exact accepted wrapper Solution for signed-out inspection and distinguishes it from the older offline adapter. The changed-hypothesis exercise asks when the weighted certificate survives a change of base or support growth. Its parameterised family is an ordinary deduction from the paper, not a separately proved Lean instance. The proof combines the linked fixed-base hereditary and all-base weighted results in the same pinned Lean environment. The pinned public Lean source contains those components; this wrapper is a composition, not a source declaration. A proved finite-deletion consequence uses the main theorem. A stronger eventual-containment consequence combines it with the finite-prefix transfer: an infinite support may contain finitely many exponents outside a binary-weighted host. The assertion for every infinite support remains open.