Local edge density n^2/50 on all half-sized vertex subsets: must the graph contain a triangle? (Erdős #128)

Let $G$ be a graph with $n$ vertices such that every induced subgraph on $\geq \lfloor n/2\rfloor$ vertices has more than $n^2/50$ edges. Must $G$ contain a triangle? (Since adding vertices to an induced subgraph only adds edges, the hypothesis is equivalent to: every vertex subset of size exactly $\lfloor n/2\rfloor$ spans more than $n^2/50$ edges.) The constant $50$ would be best possible: in the balanced blow-up of $C_5$, and in blow-ups of the Petersen graph, both triangle-free, the sparsest half-sized subsets span $n^2/50(1+o(1))$ edges.

Acceptance. FULLY RESOLVES: (a) a proof that every $n$-vertex graph in which all $\lfloor n/2\rfloor$-vertex induced subgraphs span more than $n^2/50$ edges contains a triangle — machine-checkable (Lean/Coq) preferred (a formal statement exists in formal-conjectures), else a complete written proof; computer-assisted flag-algebra proofs admissible with reproducible SDP certificates and exact rational verification; or (b) a counterexample — an explicit triangle-free graph $G$ (machine-readable, e.g. graph6) with a machine-checkable certificate that the minimum number of edges spanned by any $\lfloor n/2\rfloor$-vertex subset strictly exceeds $n^2/50$ (exhaustive check for small $n$, or a verified ILP/branch-and-bound dual certificate), plus triangle-freeness verification. ADVANCES: a proof with $1/50$ replaced by any constant strictly smaller than the best constant stated in the background ($27/1024$), with proof or reproducible certificate; removing or substantially weakening the global edge-count side conditions in the conditional results stated in the background; or certified computation of the extremal local density over all triangle-free graphs up to a new order, with exhaustive-search code and certificates. Deliver the proof file, the counterexample + certificates + checker, or the SDP/search code and verified results.