Eventual containment in a binary-weighted host forces all-base irrationality

Proved

erdos257_eventual_weighted_host_irrationality

by willcook · Sep 25, 2026 · Mathlib c5ea003 (Lean v4.30.0)

erdos-257eventual-containmentirrationalitynative-reuse

Let H be a set of positive exponents with a finite-prime weighted summability witness at base two. Let A be infinite and suppose every element of A above some cutoff N belongs to H. Then, for every integer base b at least two, the reciprocal Mersenne subseries supported on A is irrational:

\sum_{a\in A}\frac{1}{b^a-1}\notin\mathbb{Q}.

Thus the weighted-host criterion remains useful when an infinite support has finitely many exceptional exponents outside the host.

Preamble

import Definitions.Def_ErdosProblems_Erdos257_PaperCompleteR7_AnalyticTargets
import Definitions.Def_Erdos249257_CertificateKernel
import Mathlib

Formal statement

theorem erdos257_eventual_weighted_host_irrationality
    (H A : Set ℕ) (N : ℕ)
    (hH0 : 0 ∉ H)
    (hWeighted : ErdosProblems.Erdos257.PaperCompleteR7.FinitePrimeWeighted 2 H)
    (hAInf : A.Infinite)
    (hTailH : {n : ℕ | n ∈ A ∧ N < n} ⊆ H)
    (b : ℕ) (hb : 2 ≤ b) :
    Irrational (Erdos249257.erdosSupportSeries b A) := by sorry

Source

Downstream eventual-containment consequence of Will Cook’s #257 paper theorem and source finite-prefix lemma. Public main theorem: https://prove2.me/theorems/f6d332dc-466f-4f2a-a207-6b0455c0fbbd . Prefix-transfer source (Apache-2.0): https://github.com/wcook04/plectis-erdos-lean/blob/c93c2e4dd86a2e317e0cb650ea244fee1afd59c2/Erdos249257/CertificateKernel.lean#L9390-L9472 . Source paper (CC-BY-4.0; AI-assisted research disclosure): https://github.com/wcook04/plectis-erdos/blob/6917e15ec4abc2623512254da93221e446eeb707/paper/257/erdos-257-mersenne-support-subseries.tex .

View graph