ErdosProblems/263.lean: definition omits "increasing" (misformalisation vs. the corrected problem statement)

The definition of `IsIrrationalitySequence` in `FormalConjectures/ErdosProblems/263.lean`
does not include a monotonicity hypothesis:

```lean
def IsIrrationalitySequence (a : ℕ → ℕ) : Prop :=
(∀ n : ℕ, a n > 0) ∧ (∀ b : ℕ → ℕ, ...)
```

The problem at https://www.erdosproblems.com/263 was **corrected on 2026-04-02** to
require the sequence to be *increasing* ("Let $a_n$ be an increasing sequence of
positive integers..."). The correction followed DeepMind's counterexample to the
non-increasing variant (noted on the same page, in the comments).

Consequences inside the file:

1. `erdos_263.parts.ii` is tagged `category research solved` with `answer(False)`,
via a counterexample sequence that is **not increasing**. Under the corrected
statement, the increasing variant of Q2 is open (no resolution is known to us;
the site's page reflects this as of 2026-08-01).
2. Both growth variants already carry `StrictMono` as a hypothesis
(`erdos_263.variants.sub_doubly_exponential`,
`erdos_263.variants.super_doubly_exponential`), so the file currently assumes
monotonicity everywhere except in the definition and `parts.i`/`parts.ii`.
3. Koizumi (arXiv:2504.05933, footnote 1) notes Erdős–Graham originally required
strictly increasing, and the site follows that reading.

Proposed fix (happy to PR): add `StrictMono a` to `IsIrrationalitySequence`, and
re-tag or annotate `erdos_263.parts.ii` to reflect that its resolution applies to
the pre-correction statement. `erdos_263.parts.i` (`2^{2^n}`) is unaffected — that
sequence is strictly increasing either way.

Separately, we have a complete Lean 4 + Mathlib proof of
`erdos_263.variants.super_doubly_exponential` (zero `sorry`, builds on Lean
4.32.2 / Mathlib v4.32.2) hosted at https://github.com/arex1337/erdos-263-lean. If welcome, we
will PR a `formal_proof using lean4` link for that variant.

*Disclosure: the formalization and this report were produced with AI assistance
(LLM agents) under a machine-verification gate (clean `lake build`, zero `sorry`,
statement-fidelity audit against erdosproblems.com). All verification commands are
in the linked repository's README.*

References:
- https://www.erdosproblems.com/263 (statement as corrected 2026-04-02)
- Koizumi, arXiv:2504.05933 (2025), footnote 1
- Kovač–Tao, arXiv:2406.17593 (2024)

Read FormalConjectures/ErdosProblems/263.lean, starting with IsIrrationalitySequence and erdos_263.parts.i/ii, then inspect the existing StrictMono hypotheses in the growth variants. Update the definition and annotate or re-tag part ii so its status matches the corrected statement, while preserving part i, and verify the affected Lean file builds.

Written by the indexing model from the issue text.