Do $n/2$ vertices of degree $\geq n/2$ force every tree on $\leq n/2$ vertices? (Erdős #580)

Let $G$ be a graph on $n$ vertices such that at least $n/2$ of its vertices have degree at least $n/2$. Must $G$ contain every tree on at most $n/2$ vertices? Here 'contain' means: for every tree $T$ with at most $n/2$ vertices, $G$ has a subgraph isomorphic to $T$. This is the (n/2, n/2, n/2) conjecture.

Acceptance. FULLY RESOLVES: a complete proof that every $n$-vertex graph with at least $n/2$ vertices of degree at least $n/2$ contains every tree on at most $n/2$ vertices, for ALL $n$ — machine-checkable (Lean/Coq) preferred, else a full written proof; a hybrid proof (an explicit large-$n$ threshold extracted with proof, plus exhaustive machine verification below it with code and an exhaustiveness certificate) is acceptable. OR a counterexample: an explicit graph $G$ satisfying the degree hypothesis and an explicit tree $T$ on at most $n/2$ vertices, with a machine-checkable certificate (exhaustive subgraph-isomorphism search) that $G$ contains no copy of $T$. ADVANCES: (a) exhaustive verification of the conjecture for all graphs up to a stated vertex count $n$, with reproducible generation/checking code and an exhaustiveness certificate (state clearly that no prior verified bound is reported in the background); (b) an explicit numerical threshold $n_0$ for Zhao's theorem, with proof; (c) a proof for a new structured class of graphs or trees (e.g. all spiders or all bounded-degree trees, for all $n$) strictly beyond what the background states. Deliver the proof file, or the code + verified range + certificate, or the counterexample pair + certificate.