Solved, the site's label. Boon Suan Ho, working with GPT-5.4 Pro, characterized the attainable growth: for non-decreasing $F\to\infty$, some admissible $S$ has measure at least $F(x)$ in $(0,x)$ for all large $x$ exactly when $\int_1^\infty F(x)x^{-2}\,dx<\infty$. The accepted claim is Ho's sharp growth criterion, credited by the site's curator and not refereed; a Lean formalization in Boris Alexeev's repository is linked on the claim page, and this corpus has not built or audited it.