PROVED (FORMALIZED), the site's label as printed on 2026-09-05; the community database (record of 2026-10-06) lists the status proved (Lean) as of its last update on 3 September 2026; the page, last edited 7 September 2026, printed no label in its static text on 2026-10-07. Both readings of the Statement (Formulation) are proved, so the problem is settled. The consequence of the sharp tree-free bound in #548, whose proof the site's proof-claim entry credits to GPT-6 Astra, gives the explicit Ramsey corollary $R_k(T)\leq k(n-2)+2$ for $k\geq1$ and $n\geq2$ without a threshold, one constant for every $k$ and every tree, which proves both readings. That consequence is the accepted full claim recorded on the claim page Adamczewski 2026 on a third party's Lean derivation of it that this corpus built and audited (Formalization, below); the credit of the site's curator for it was not independent, since he submitted the proof claim himself and co-authored the paper recording the result, and nothing is refereed. The frontmatter standing, solved and proved, derives from it. Reed and Stein's dense case of the Erdős--Sós conjecture (arXiv:2609.05417, 4 September 2026) gives, for each $k$, an $n_0(k)$ with $R_k(T)<k(n-2)+3$ for every tree $T$ on $n\geq n_0(k)$ vertices, hence $R_k(T)\leq kn+O_k(1)$, which proves reading (a) only; the site's commentary of 7 September 2026 credits that theorem and the deduction, so the claim page Reed and Stein 2026 is an accepted partial claim on the curator's credit.