Erdős 257: add the coprimality-free summable-support theorem (Erdős 1968, p. 222, stated without proof)

`FormalConjectures/ErdosProblems/257.lean` currently carries `erdos_257` (research open), `erdos_257.variants.tsum_top_eq` (textbook, proved), and `erdos_257.variants.tsum_top` (research solved).

I would like to add one further variant:

For every integer $b \ge 2$ and every infinite $A \subseteq \mathbb{N}$ with $\sum_{a \in A} 1/a < \infty$, the number $\sum_{a \in A} 1/(b^a - 1)$ is irrational. There is no coprimality, periodicity, or density hypothesis.

Erdős, *On the irrationality of certain series*, Math. Student 36 (1968), 222-226, proves this on p. 222 for pairwise coprime $A$ at every integer base $b \ge 2$. The next sentence of that paper states that pairwise coprimality can be removed by a more complicated argument, which is not printed there; p. 226 repeats the boundary. I have a Lean proof of the coprimality-free statement, sorry-free, with axiom set exactly `[propext, Classical.choice, Quot.sound]`.

The proof is long, so under CONTRIBUTING it stays external and the upstream declaration is linked with `@[formal_proof using lean4 at ...]`. The link target is a bridge theorem stated token-identically to the proposed upstream statement.

The variant is relevant to `erdos_257` itself: it implies that any counterexample support has divergent reciprocal mass. It does not decide `erdos_257`.

I will open a pull request against this issue.

Start in FormalConjectures/ErdosProblems/257.lean and compare the existing erdos_257 variants. Add the coprimality-free summable-support theorem using the externally linked bridge declaration, and verify that the resulting formalization is sorry-free with axiom set exactly [propext, Classical.choice, Quot.sound].

Written by the indexing model from the issue text.