Erdős 243: add Koizumi's Sylvester and Millin rigidity corollaries

[wcook04]

Closes #5058.

243.lean currently holds only the open statement. Koizumi,
arXiv:2504.05933 (2025), studies exactly
this problem — his Question 5 (p. 3) is Erdős 243 verbatim — and proves two
rigidity corollaries this adds.

erdos_243.variants.sylvester_of_tsum_eq_one (his Corollary 2, p. 2): if
$2/3 \le a_n^2/a_{n+1} \le 4/3$ and $\sum 1/a_n = 1$, then $a_n$ is Sylvester's
sequence $2, 3, 7, 43, 1807, \dots$. The contrast with erdos_243 is the point:
there the ratio tends to $1$ and the sum is merely rational, and the
conclusion is an eventual recurrence; here a two-sided bound plus an exact sum
pins the sequence down at every index.

erdos_243.variants.fib_of_tsum_eq_millin (his Corollary 3): if
$a_n^2/a_{n+1} \le 2/3$ and $\sum 1/a_n = (5-\sqrt5)/2$, then $a_n = F_{2^n}$.

erdos_243.sylvester_satisfies_recurrence — a one-line test recording
that Sylvester's sequence satisfies the recurrence in the conclusion of
erdos_243, so the two statements are visibly about the same recurrence.

Sylvester's sequence is not in Mathlib, so
FormalConjecturesForMathlib/NumberTheory/Sylvester.lean defines it with basic
API (two_le_sylvester, strictMono_sylvester, and the first values). That
file is fully proved — no sorry, and every declaration audits to
[propext, Classical.choice, Quot.sound] or less.

Checks:

• Builds clean against current main (33c6a2d): 0 errors, 0 warnings.
• Both corollaries were checked numerically against their claimed witnesses
  before formalising. Sylvester gives ratios
  $4/3, 9/7, 49/43, 1849/1807$ — all in $[2/3, 4/3]$, with $s_1^2/s_2 = 4/3$
  meeting the bound exactly — and $\sum 1/s_n = 1$. The Fibonacci witness gives
  ratios converging to $1/\sqrt5 \approx 0.447 \le 2/3$ and
  $\sum 1/F_{2^n} = 1.381966011250105 = (5-\sqrt5)/2$.
• The same paper's Theorem 4 is already cited in 263.lean; these corollaries
  are not used there.

No originality is claimed — the theorems are Koizumi's. The contribution is
their formal statement plus the Sylvester definition needed to express them.

AI Usage Disclosure: this contribution was produced with AI assistance. I have
read the corollaries in the source paper, checked the index conventions against
his $n \ge 1$ numbering, verified the witnesses numerically, and reviewed this
diff, and I take responsibility for the submission.

Note

These are adjacent solved results, not special cases of erdos_243, which
remains open and is untouched.

[wcook04]

Note for whoever merges this: #5038, #5041 and #5059 each add one public import line to FormalConjecturesForMathlib.lean in the same alphabetical slot (after SmoothScale, before WallSunSunPrimes). They are independently mergeable against main. Merging one will need a one-line rebase on the other two. The new ForMathlib files themselves do not overlap.