Erdős 257: settled support families, and the structure of the value space

[wcook04]

Closes #5054.

This is the single Erdős 257 PR. It supersedes #5033, #5040 and #5047, which I have closed — every declaration from all three is preserved here verbatim, with its own proof link.

They were separate PRs by mistake on my part. 257.lean is one file that each contribution appends to, so four PRs against it conflict by construction rather than by accident; splitting them created work for a reviewer and none of it was mine to hand over.

erdos_257 itself is untouched and remains open.

What the file now contains, in order

The open question, then what is settled about it:

Declaration	Says
eventually_periodic_support	eventually periodic infinite supports give irrational sums
pairwise_coprime_support	so do infinite pairwise-coprime supports with summable reciprocals
factorial_support	so does the positive-factorial support
two_pow_support	so does the powers-of-two support

These four are stated in the same shape erdos_257 uses — ∑' n : A, 1 / (b ^ n - 1) — so they need no new vocabulary, and the base is generalised from 2 to any integer b ≥ 2.

The classical identities, tsum_top_eq and tsum_top, the latter now carrying the formal proof from #5033.

Structural results:

Declaration	Says
finite_period_noncollapse	for a finite support, the multiplicative order of the base modulo the reduced denominator is exactly the lcm of the support
support_measure_dichotomy	the support-restricted achievement set has measure 2^(-|F|) for finite omitted F, and 0 when infinitely many are omitted
supported_achievement_set_geometry	that set is also injectively coded, compact, totally disconnected and nowhere dense — and perfect when J is infinite

The last two share the six definitions in FormalConjecturesForMathlib/NumberTheory/MersenneAchievementSet.lean, the only support file this PR adds.

The geometry statement is given for arbitrary J rather than only the full set. IsTotallyDisconnected unfolds to a condition quantified over subsets, so it descends along ⊆ exactly as nowhere density does; at J = Set.univ it therefore is the full-set statement, with unique coding as its injectivity conjunct. IsClosed is deliberately not a conjunct — the set is a compact subset of ℝ and Perfect already carries closedness.

Prior art

None of the mathematics here is new, and no claim of novelty or priority is made for any of it.

• Eventually periodic supports are the $0$–$1$ coefficient case of Luca–Tachiya, doi:10.1142/S1793042113501121.
• Pairwise-coprime supports are Erdős, On the Irrationality of Certain Series, Math. Student 36 (1968), 222–226, theorem on p. 222.
• The factorial and powers-of-two families sit in the rapid-growth framework of Erdős–Straus, J. Indian Math. Soc. 27 (1964), 129–133; the powers-of-two case is their Example 1. Duverney later proved that value transcendental (doi:10.1017/S0305004100004783); what is recorded here is irrationality.
• Kovač–Tao (doi:10.1007/s10474-025-01528-0, Remark 4.1) prove the strict-tail inequality for these exact weights and record both the unique coding and the Cantor-set conclusion; the achievement-set topology is classical, going back to Kakeya. The measure computation is the part their remark does not carry.

Receipts

• lake build 'FormalConjectures.ErdosProblems.«257»' succeeds on this branch.
• The linked adapter is compiled by CI in the source repository, not only locally: https://github.com/wcook04/plectis-lean-erdos249-257/actions/runs/32196665233 (Build foreign-corpus variant candidates → lake build FormalConjecturesVariants, green on main).
• Every linked declaration audits to [propext, Classical.choice, Quot.sound]. There is no sorryAx.
• Each upstream statement was diffed textually against the adapter declaration its permalink points at; all match. This matters because the upstream bodies are sorry, so nothing else enforces that the link proves the stated proposition.
• Negative control: replacing Nat.factorial (k + 1) by Nat.factorial k is rejected with a type mismatch, so the index convention is load-bearing rather than incidental.
• Proofs are hosted externally per CONTRIBUTING.md and linked at immutable commits.

AI Usage Disclosure: the linked Lean development and this contribution were produced with AI assistance. I have reviewed the statement identity of every variant against its proof, the axiom reports, the attributions above, and this diff, and I take responsibility for the submission.

Note

These are solved variants and settled support families around Erdős 257. They do not prove irrationality for every infinite support, so erdos_257 remains open and is untouched.