Erdős 1049: add the Bundschuh–Väänänen rational-base criterion

[wcook04]

Closes #5056.

This is the single Erdős 1049 PR. It supersedes #5032: geq_2_integer now carries the formal_proof permalink from that PR.

1049.lean records Erdős's 1948 theorem for integer bases $t \ge 2$ and
nothing for non-integer rational $t$. This adds the published criterion that
covers part of that gap, and the Lean proof link for the integer-base case.

erdos_1049.variants.geq_2_integer — Erdős [Er48] for integer $t \ge 2$.
The statement was already here; this PR attaches
formal_proof using lean4 at the existing sorry, pointing at the Lean 4 proof
in wcook04/plectis-lean-erdos249-257.

erdos_1049.variants.bundschuh_vaananen — Bundschuh and Väänänen,
Arithmetical investigations of a certain infinite product, Compositio Math.
91 (1994), 175–199, Theorem 2 (printed p. 177): "In the special case
$\alpha = -1$ we may even allow $\lambda < (1/2 + 1/\pi^2)^{-1}$." Their
$L_q(\alpha) = \sum_{j\ge1}(q^j+\alpha)^{-1}$ (p. 177), so $\alpha = -1$ gives
exactly this problem's series, and $\lambda = \log h(q)/\log|q|$ from Theorem 1.
For $t = a/b &gt; 1$ in lowest terms, $\lambda = \log a/\log(a/b)$, and the
condition rearranges to

$$\frac{\log b}{\log a} < \frac12 - \frac1{\pi^2}.$$

Stated with t.num and t.den, so coprimality and positivity come from the
type. At $b = 1$ the hypothesis reads $0 &lt; 1/2 - 1/\pi^2$, so this statement
contains erdos_1049.variants.geq_2_integer. This is a literature statement,
kept by sorry per the repository's convention; there is no Lean proof of the
general criterion to link.

erdos_1049.variants.seven_halves — the criterion applies at $t = 7/2$,
giving irrationality at a non-integer base. Proved from the above via
$\log 2/\log 7 &lt; 9/25 &lt; 1/2 - 1/\pi^2$, the first inequality because
$2^{25} = 33{,}554{,}432 &lt; 40{,}353{,}607 = 7^9$, the second because $\pi^2 &gt; 9$.

erdos_1049.variants.bundschuh_vaananen_fails_at_three_halves — the
criterion does not reach $t = 3/2$, since $\log 2/\log 3 &gt; 1/2 &gt; 1/2 - 1/\pi^2$
(the first inequality because $3 < 2^2). This marks the frontier: the smallest non-integer rational base is outside the published range, and erdos_1049` is
open there.

Checks:

• The touched module builds with 0 errors and 0 warnings under the Formal
  Conjectures linters (copyright, namespace, stubs, openClassical,
  ams_attribute, category_attribute, conditional_formal_proof,
  moduleDocstring, latex_docstring, imports).
• bundschuh_vaananen_fails_at_three_halves depends on
  [propext, Classical.choice, Quot.sound] only — no sorryAx. The Bundschuh–Väänänen
  criterion itself is a literature statement, by sorry. geq_2_integer remains
  by sorry with a formal_proof link, as the linter requires.
• $7/2$ is the smallest denominator-$2$ base the criterion reaches: the only
  candidates below it are $3/2$ and $5/2$, and both fail.

No originality is claimed for any of this; the criterion and its proof are
Bundschuh and Väänänen's, and the integer-base proof is Erdős 1948 as
formalised in the linked repository. The contribution is the formal statement,
its reduction to a condition on t.num and t.den, the two proved statements
locating the boundary, and the proof link on the existing integer-base variant.

AI Usage Disclosure: this contribution was produced with AI assistance. I have
read Theorem 2 in the source paper, checked the reduction of $\lambda$ to the
stated condition, verified the numeric inequalities, and reviewed this diff, and
I take responsibility for the submission.

Note

This covers a proper subset of the rational bases. erdos_1049 remains open
and is untouched.