Claims

../

2016_08_14_tidor_wang_yang: The 2016 inequality that some monotone subsequence of distinct reals has sum at least the root of the sum of squares of the positive terms, which gives the lower bound c at least 1; the first proof, as the site's curator credits.

2025_12_07_alexeev: A Lean proof generated by Aristotle, posted by Boris Alexeev in December 2025, of the k-squared statement and then of the exact least ratio c(n) for every n, so c equals 1; credited by the curator; the corpus has not built it.

---