The site's label is PROVED (LEAN). For every $a\ge1$ such a $b$ exists and $b(a)$ grows linearly: van Doorn's Corollary 1 gives $b(a)\le6(a-1)$ for $a>1$ and his Theorem 2 gives $b(a)\le4.374(a-1)$ for $a\ge6$, both in his convention; Corollary 1 comes from the $3$-adic valuation of the block ending at $2\cdot3^{k+1}$, and Theorem 2 from a computer-checked table of endpoints for $a\le3^{10}$ and $3$-adic valuations at endpoints chosen on six subintervals of $(3^k,3^{k+1}]$ beyond. This is the accepted claim van Doorn 2024, an arXiv paper without a journal version, credited by the site's curator, with an external Lean proof of the existence statement of which no build is recorded; its value is solved because the problem pairs a yes-or-no question with a growth question and the paper answers both, the first with a proof and the second with a two-sided estimate. The finer growth of $b(a)-a$ is of order $\log a$ at its smallest, $a+0.54\log a<b(a)$ for all large $a$ and $b(a)<a+0.61\log a$ for infinitely many $a$ (Theorem 8), and is the subject of two pending partial claims by the same author: the exact value $\liminf_{a\to\infty}(b(a)-a)/\log a=1/(1+c)\approx0.546$ (2026 preprint) and the almost-all lower bound $b(a)>a+\exp(\tfrac12\sqrt{\log a\log\log a})$ (2026 note). No upper bound below linear appears in a manuscript; a thread comment of 24 September 2026 sketches $b(a)-a\ll a^{61/80}$ (see the forum items below). The site's Lean suffix is a catalog label explained under Formalization.