Is the sum of 1/(2^n-1) over every infinite set of positive exponents irrational?
Statements and boundaries are copied from the corpus record. Registry status: not_registered; the claim registry does not carry these declarations and kernel checking them does not promote them into reviewed public claims
The base-2 Mersenne achievement set has Lebesgue measure exactly one.
This does not decide whether every infinite-support sum is irrational.
For every integer base b >= 2, the full-support Erdos-Borwein series is irrational.
This is the classical full-support theorem, not universal Erdos #257.
For a reduced finite Mersenne sum, the base order modulo the denominator equals the support lcm.
The finite-support theorem does not settle any infinite-support sum.
A support-restricted Mersenne achievement set has exact finite-complement measure or measure zero for infinite complement.
The measure dichotomy does not classify rational points.
Prove any one of these and the corresponding reduction above becomes unconditional.
arithmetic_rigidity_for_thin_supports Convert hereditary unique coding into an arithmetic obstruction to rational values for every infinite support, including zero-measure Cantor supports.formalise_measure_and_stride_geometry Extend the measure dichotomy to Bernoulli laws and periodic-stride dimensions without implying arithmetic consequences.| Module | Lines | Declarations | Theorems |
|---|---|---|---|
ErdosProblems.Erdos257.MersenneSubseriesRigidity |
421 | 28 | 23 |
The Comparator replays selected exact interfaces against a pinned toolchain. It never widens what Lean proved.
Statement and type parity replayed against the pinned toolchain.
The multiplicative order of the base modulo a reduced finite-sum denominator is the support lcm, forcing denominator growth.
A finite-support denominator theorem does not settle an infinite-support sum.
finite_period_noncollapse · targeted
Full, factorial, power-of-two, multiple, pairwise-coprime, eventually periodic, residue-class, and odd supports are formalised.
Structured known families do not cover arbitrary infinite supports.
known_irrational_supports · targeted_full_support_representative
Compactness, perfectness, total disconnectedness, nowhere density, and measure one for the unrestricted achievement set.
Geometry of the full set does not decide irrationality of every coded point.
achievement_set_geometry · targeted_measure_theorem
Support-restricted coding is injective and the associated achievement set has exact finite-complement measure or zero for infinite complement.
The measure dichotomy does not classify rational points.
restricted_achievement_sets · targeted_measure_dichotomy
Stated in the corpus; not part of the replayed interface set.
Rational infinite supports force unbounded scaled tails, sublogarithmic zero windows, and reciprocal-mass constraints.
The constraints do not exclude every infinite support.
rational_support_constraints · not_selected_deep_support_vocabulary
Lean checks squarefree incidence and no-go statements; the irrationality conclusion uses an external analytic theorem in the paper.
Comparator must not badge the paper-plus-external conclusion.
squarefree_support · not_applicable_to_external_irrationality_input
Exact greedy characterisations and finite-support exclusions isolate the remaining 1/2 and 1/21 alternatives.
Neither membership question is decided.
half_and_twenty_one_frontiers · not_selected_deep_greedy_state_vocabulary
Denominator Periods, Rational-Value Constraints and Achievement-Set Geometry
For every finite support and integer base, the reduced denominator has multiplicative order exactly the support lcm. Restricted achievement sets also receive exact coding, topology, perfectness, and measure statements with their finite/infinite hypotheses. Rational infinite supports must satisfy explicit long-division and divisor-incidence constraints, but those constraints do not conflict. Prime support at base 2 and squarefree support at power-of-two bases are cited prior results, not contributions here. The targets 1/2 and 1/21 reduce to open infinite-orbit alternatives; Erdős #257 remains open.