DISPROVED (LEAN), the site's label, which describes the Statement as printed. The witness is the one the site's commentary names, a complete bipartite graph whose smaller side has about $n^\alpha$ vertices, recomputed here in the Current assessment: for $0<\alpha<\tfrac12$, every $\epsilon>0$ and every $D\ge1$, the graph $K_{a,n-a}$ with $a=\lceil2n^\alpha\rceil$ has at least $n^{1+\alpha}$ edges for large $n$, and every $D$-balanced subgraph of it with an edge has at most $(D+1)a<n^{1-\alpha}$ vertices, so no $D$-balanced subgraph on more than $n^{1-\alpha}$ vertices has any edge. As a universal statement over $\epsilon$ and $\alpha$ the Statement is therefore false; for $\alpha\ge\tfrac12$ this witness gives nothing and the page decides nothing. The failure holds for every $0<\alpha<\tfrac12$, not only at boundary values, and the exponent $1-\alpha$ is the poser's explicit print, so the curator's guess at the intended question is a variant (Formulation) and not a correction. A Lean file refutes the collection's formal statement with the same family at $\alpha=\tfrac14$, and with it the printed wording, which implies that statement; the corpus built the file and audited its statement (Formalization). The claim pages record the complete bipartite witness of 28 December 2025 (JunGao), the clique counterexample of 24 December 2025 (clique counterexample) and the Lean file (Lean file). JunGao's witness carries the site's acceptance, since the site's label and commentary credit JunGao and the complete bipartite graph; the Lean file's acceptance rests on the corpus's build and statement audit; the clique construction, which neither the site nor a build credits, is claimed.